Trm_ind@{i j k | i <= k, j < k} {A : Type@{i}} `{Funext} {P : Trm@{i j} A -> Type@{j}} {p : forall x, IsHProp@{j} (P x)} (f : forall a, P (trm a)) : forall x, P x. Proof. unfold Trm. intro x. rapply x. intro a. refine (transport P _ (f a)). rapply path_ishprop@{k}. Defined.
Require Import HoTT.Basics. Require Import Universes.Smallness.