The Coq mailing list

[coqcdp <coqcdpnxj AT 163.com>]

yes,thanks very much. It all works.
At 2014-08-01 00:54:11, "Matej Kosik" 
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
 wrote:
>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?