The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

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?

Sincerely,