Lemma hexistsnegtonegforall {X : UU} (F : X -> UU) : (∃ x : X, neg (F x)) -> neg (∏ x : X, F x). Proof. simpl. apply (@hinhuniv _ (make_hProp _ (isapropneg (∏ x : X, F x)))). simpl. intros t2 f2. induction t2 as [ x d2 ]. apply (d2 (f2 x)). Defined.