Theorem isofhlevelfsnfib (n : nat) {X : UU} (P : X -> UU) (x : X) (is : isofhlevel (S n) (x = x)) : isofhlevelf (S n) (tpair P x). Proof. intros. unfold isofhlevelf. intro xp. apply (isofhlevelweqf (S n) (ezweq1pr1 P x xp)). apply isofhlevelsn. intro X1. induction X1. assumption. Defined.