I have following unfinished proof of a lemma:
Goal forall (P : Type -> Prop) (Q : Prop), ((forall x, (P x)) -> Q) -> (exists x, P x -> Q). Proof. intros. eapply ex_intro. intros. apply H. intros. eapply H0.
The problem is the last
eapply failed, with the message
Error: In environment P : Type -> Prop Q : Prop H : (forall x : Type, P x) -> Q H0 : P ?x x : Type Unable to unify "?x" with "x" (cannot instantiate "?x" because "x" is not in its scope: available arguments are "P" "Q" "H").
The proof steps themselves look very phishy already. The proof constructs an existential variables to sit in place of $x$ in the second half, and then tries to instantiate it using the $x$ obtained as premise after applying the hypothesis
(forall x, (P x)) -> Q. The proof steps look cyclic proof to me.
What in general does this message imply? What types of logical mistake does this message indicate here?
There is a recent github issue from Coq actually indicates that instantiating evars outside of scope CAN prove falsehood, except that it's blocked by QED.