Theorem isofhlevelffib (n : nat) {X : UU} (P : X -> UU) (x : X) (is : ∏ x' : X, isofhlevel n (x' = x)) : isofhlevelf n (tpair P x). Proof. intros. unfold isofhlevelf. intro xp. apply (isofhlevelweqf n (ezweq1pr1 P x xp) (is (pr1 xp))). Defined.