Some lemmas on property of rewriting. It will probably be worth at

some time to provide a library stating the groupoid structure of
equality proofs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15976 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 0 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 17d712246..77af30dcb 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -355,12 +355,34 @@ End Logic_lemmas.
 Module EqNotations.
   Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H)
     (at level 10, H' at level 10).
+  Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+    (at level 10, H' at level 10).
   Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H)
     (at level 10, H' at level 10).
+  Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H)
+    (at level 10, H' at level 10).
   Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H)
     (at level 10, H' at level 10, only parsing).
+  Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
+    (at level 10, H' at level 10).
 End EqNotations.
 
+Import EqNotations.
+
+Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
+Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a.
+Proof.
+intros.
+destruct H.
+reflexivity.
+Defined.
+
 Theorem f_equal2 :
   forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
     (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.