From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 2 Mar 2010 16:39:15 +0000 (+0000)
Subject: Added reverse rewriting principle in Type[0].
X-Git-Tag: make_still_working~3019
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a2b0d520b7863694130de56c5bf30fdd07696bd;p=helm.git

Added reverse rewriting principle in Type[0].
---

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index f1a679c7d..fa93f4f1b 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -18,6 +18,16 @@ include "properties/relations.ma".
 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  refl: eq A a a.
 
+nlemma eq_rect_Type0_r':
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
+ #A; #a; #x; #p; ncases p; #P; #H; nassumption.
+nqed.
+
+nlemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
+nqed.
+
 nlemma eq_rect_CProp0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
@@ -182,6 +192,7 @@ match x return (λr1,r2,r.
                    → P);
 
 
+
 ndefinition i2d : ∀a,b.∀x,y:I2 a b.
                   ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
                   ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝