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).
Tento fazer isso de muitas maneiras diferentes e não sei o que há de errado. Esta é minha última tentativa:
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.
mas produz este erro: No ambiente P, Q: Set -> Prop f: Set -> Set x: Set H1: P x -> Q (fx) x0: Set H2: P x0 Incapaz de unificar "Q (fx) " com "Q (f x0)".