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