Theorem impred (n : nat) {T : UU} (P : T -> UU) : (∏ t : T, isofhlevel n (P t)) -> (isofhlevel n (∏ t : T, P t)). Proof. revert T P. induction n as [ | n IHn ]. - intros T P X. apply (funcontr P X). - intros T P X. unfold isofhlevel in X. unfold isofhlevel. intros x x'. assert (is : ∏ t : T, isofhlevel n (x t = x' t)) by (intro; apply (X t (x t) (x' t))). assert (is2 : isofhlevel n (∏ t : T, x t = x' t)) by apply (IHn _ (λ t0 : T, x t0 = x' t0) is). set (u := toforallpaths P x x'). assert (is3: isweq u) by apply isweqtoforallpaths. set (v:= invmap (make_weq u is3)). assert (is4: isweq v) by apply isweqinvmap. apply (isofhlevelweqf n (make_weq v is4)). assumption. Defined.