Corollary impredtwice (n : nat) {T T' : UU} (P : T -> T' -> UU) : (∏ (t : T) (t': T'), isofhlevel n (P t t')) -> (isofhlevel n (∏ (t : T) (t': T'), P t t')). Proof. intros X. assert (is1 : ∏ t : T, isofhlevel n (∏ t': T', P t t')) by (intro; apply (impred n _ (X t))). apply (impred n _ is1). Defined.