The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

On 30/07/14 09:30, coqcdp wrote:
> Hi,
>        The context of my program  is 
>                                           s:U->U->U.
>                                           a:U.
>                                           b:U.
>                                           c:U.
>                                         H0: forall a0 b0 c0:U,s (s a0 b0) 
> c0=s a0 (s b0 c0).
>                                        H1:forall a0 b0:U,s a0 b0 = s b0 a0.
>                          
> _________________________________________________________________
>                                              s b ( s c a) = s b ( s a c)
> 
> I want to use "rewrite H1" strategy to rewrite " s c a " to " s a c" ，but 
> it doesn't work.  Could you tell me the reason and give me some proper 
> suggestions?  Thank you very much.

A few days ago I asked a question about rewrite tactic, because I was also 
puzzled.

I am not sure if I understand your difficulty, but, did you try:

        rewrite (H1 c a).

or

        pattern (s c a).
        rewrite H1.

?

In both cases I am getting:

        s b (s a c) = s b (s a c)

Is this what you wanted?