Theorem isapropisofhlevel (n : nat) (X : UU) : isaprop (isofhlevel n X). Proof. revert X. induction n as [ | n IHn ]. - apply isapropiscontr. - intro X. apply impred. intros t. apply impred. intros t0. apply IHn. Defined.