resized_Trm_rec_beta@{i j k u | i <= k, Set < k} {A : Type@{i}} {P : Type@{j}} `{IsHProp P} (f : A -> P) : resized_Trm_rec@{i j k u} f o resized_trm == f. Proof. intro a. unfold resized_Trm_rec, resized_trm, Trm, trm; cbn beta. rewrite eisretr@{u k}. apply eisretr@{Set j}. Defined.
Require Import HoTT.Basics. Require Import Universes.Smallness.