Lemma forallnegtoneghexists {X : UU} (F : X -> UU) : (∏ x : X, neg (F x)) -> neg (∃ x, F x). Proof. intros nf. change ((ishinh_UU (total2 F)) -> hfalse). apply hinhuniv. intro t2. induction t2 as [ x f ]. apply (nf x f). Defined.