The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 21 Jan 2013 16:26:15 -0300,
Leonardo Rodriguez 
<leonardomatiasrodriguez AT gmail.com>
 a écrit :

> 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!

assert (<name_you_want_to_give> := H x0).

I think it is in the documentation.
Check the "assert" tactics to find out all the variants (mainly set and
pose). There is also the "cut" tactic. It is not the same as assert,
but desserves some similar goal.

cut makes you assume some hypothesis, and require you to prove your
goal in this context, then prove your hypothesis, while assert requires
you to first prove your hypothesis, then prove your goal (the order is
reversed).