Lemma x: forall P Q: Set -> Prop,
forall f: Set -> Set,
forall x, (P x -> Q (f x)) ->
(exists x, P x) -> (exists x, Q x).
我尝试了很多不同的方法，但我不知道哪里出了问题。这是我的最新尝试：
Lemma x: forall P Q: Set -> Prop,
forall f: Set -> Set,
forall x, (P x -> Q (f x)) ->
(exists x, P x) -> (exists x, Q x).
Proof.
intros P Q f x H1 [x0 H2].
exists (f x0).
apply H1.
assumption.
Qed.
但它会产生以下错误： 在环境 P, Q : Set -> Prop f : Set -> Set x : Set H1 : P x -> Q (fx) x0 : Set H2 : P x0 Unable to unify "Q (fx) ”与“Q (f x0)”。