proposition: Lemma ex_func (A : Type) (P Q : A -> Prop) : (forall x, P x -> Q x) -> (exists x, P x) -> (exists x, Q x).
proof: Proof. intros allx_Px_to_Qx somex_Px. destruct somex_Px as [x Px]. exists x. exact (allx_Px_to_Qx x Px). Qed.
imports: Classical_Prop Classical_Pred_Type