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