Skip to Content.
Sympa Menu

coq-club - [Coq-Club] problem to rewrite

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem to rewrite


Chronological Thread 
  • From: coqcdp <coqcdpnxj AT 163.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] problem to rewrite
  • Date: Wed, 30 Jul 2014 16:30:07 +0800 (CST)

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.





Archive powered by MHonArc 2.6.18.

Top of Page