The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael wrote:
>   apply asr_2 with (x:=1000) (y:=1) (z:=4).
> Save.
>
> This, however, gives me the error:
> Impossible to unify "asr 1000 (1+4) = asr (asr 1000 1) 4" with "1<= asr 10000
> 5)". How can I apply the Lemmas to solve "test1"?
>    

You probably want [rewrite] instead of [apply], and you might need to 
[change] the conclusion first so that [rewrite] knows the conclusion 
matches your lemma.  Please see the manual entries on these tactics.