The Coq mailing list

[coqcdp <coqcdpnxj AT 163.com>]

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.

 

Yours Sincerely ,

                             D.P.Chen.