proposition: Lemma ex_not_all_func (A : Type) (P Q : A -> Prop) : (forall x, Q x -> ~P x) -> (exists x, Q x) -> (~forall x, P x).
proof: Proof. intros allx_Qx_to_notPx somex_Qx. apply ex_not_not_all. destruct somex_Qx as [x Qx]. exists x. exact ((allx_Qx_to_notPx x) Qx). Qed.
imports: Classical_Prop Classical_Pred_Type