In Coq (or Rocq), can't a lemma with a universal conclusion be applied to other premises?

When I prove with Coq (or Rocq), I find that sometimes if a hypothesis is "P" and another is "P -> forall x, Q x", I cannot make "forall x, Q x" a new premise by modus ponens.

Here is an example:

Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
  (P -> forall x, Q x) -> forall x, P -> Q x.
Proof.

(* 
Here is a correct proof:

intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H.
apply H1. 
Qed.
*)


intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H in H1.
(** STUCK HERE, 

But Why cannot we do this???

They look the same.
*)
Admitted.

The proof will be stuck in the line "apply H in H1" and Coq returns that "Unable to find an instance for the variable x."

But must "x" be instantiated? It looks unnecessary. What is the difference between the two proofs?

I asked both DeepSeek and ChatGPT. Neither of them could provide a satisfiable answer.

I also guessed that it could be the variable occurrence problem in the antecedent. But if it were, the tactic "generalize dependent" should have failed.

Answer

See Read more: a simple fix is to use eapply H in H1, or just conclude the proof with exact (H H1).

Alternatively, note that you don't really need tactics here: the whole proof is just fun X P Q H x p => H p x.