proposition: Lemma isofhlevelsnprop (n : nat) {X : UU} (is : isaprop X) : isofhlevel (S n) X.
proof: Proof. simpl. unfold isaprop in is. simpl in is. intros x x'. apply isofhlevelcontr. apply (is x x'). Defined.
imports: UniMath.Foundations.PartA