The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael wrote:
> I have a proof Y, and at some point used the tactic "generalize H0", resulting
> in a verification condition "X ->  Y". Now I have a Lemma Lem1 of the form "A 
> ->
> B ->  C", which matches X with C. I'd like to apply Lem1 to the first part 
> (X).
> However, "apply Lem1" results in an error. It seems to me Coq tries to match 
> "B
> ->  C" with "X ->  Y", but that's not what I wanted. How can I apply the 
> Lemma in
> the way I need it?
>    

I think the simplest way is [intro Hx; apply Lem1 in Hx].