The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi club,
an interesting question was asked on StackOverflow yesterday, and I
have to say I don't understand why this simple apply fails. Consider
the script:

Parameter P: nat -> Prop.
Parameter Q: nat -> Prop.
Hypothesis x : forall i, P i -> (forall k, Q k).

Lemma y:
  forall i, P i -> (* Whatever *) P i.
Proof.
  intros i hPi.
  apply x in hPi.

It fails with: Error: Unable to find an instance for the variable k.

Why does Coq asks for the instantiation of k ?

Best,
V.