Theorem hlevelntosn (n : nat) (T : UU) (is : isofhlevel n T) : isofhlevel (S n) T. Proof. revert T is. induction n as [ | n IHn ]. - intro. apply isapropifcontr. - intro. intro X. change (∏ t1 t2 : T, isofhlevel (S n) (t1 = t2)). intros t1 t2. change (∏ t1 t2 : T, isofhlevel n (t1 = t2)) in X. set (XX := X t1 t2). apply (IHn _ XX). Defined.