proposition: Lemma isofhlevel_hsubtype {X : UU} {n : nat} (isof : isofhlevel (S n) X) : ∏ subt : hsubtype X, isofhlevel (S n) subt.
proof: Proof. intros subt. apply isofhleveltotal2. - assumption. - intro. apply isofhlevelsnprop. apply propproperty. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics