The Coq mailing list

[Leonardo Rodriguez <leonardomatiasrodriguez AT gmail.com>]

Hello,

Suppose you have  some hypotheses like 

H : forall x y, P x y
x0 : A

and you want a new hypothesis like

H0 : forall y , P x0 y.

In that kind of situation I usually do

assert (forall y , P x0 y)
apply H.

but .. Is there a better way to do this? 

I'm relatively new in Coq .
Thank you!