Definition weqforallnegtonegexists {X : UU} (F : X -> UU) : (∏ x : X, ¬ F x) ≃ (¬ ∃ x, F x). Proof. intros. apply (weqimplimpl (forallnegtoneghexists F) (neghexisttoforallneg F)). apply impred. intro x. apply isapropneg. apply isapropneg. Defined.