proposition: Lemma not_all_ex_func (A : Type) (P Q : A -> Prop) : (forall x, ~P x -> Q x) -> (~forall x, P x) -> (exists x, Q x).
proof: Proof. intros allx_notPx_to_Qx notallx_Px. apply not_all_ex_not in notallx_Px. destruct notallx_Px. exists x. apply allx_notPx_to_Qx. assumption. Qed.
imports: Classical_Prop Classical_Pred_Type