Corollary isofhlevelcontr (n : nat) {X : UU} (is : iscontr X) : isofhlevel n X. Proof. revert X is. induction n as [ | n IHn ]. - intros X X0. assumption. - intros X X0. simpl. intros x x'. assert (is : iscontr (x = x')). apply (isapropifcontr X0 x x'). apply (IHn _ is). Defined.