Lemma isofhlevelssn (n : nat) {X : UU} (is : ∏ x : X, isofhlevel (S n) (x = x)) : isofhlevel (S (S n)) X. Proof. intros. simpl. intros x x'. change (∏ (x0 x'0 : x = x'), isofhlevel n (x0 = x'0)) with (isofhlevel (S n) (x = x')). assert (X1 : x = x' -> isofhlevel (S n) (x = x')) by (intro X2; induction X2; apply (is x)). apply (isofhlevelsn n X1). Defined.