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 f1a679c7d5dbf8719122139793871eed8e77abf8..fa93f4f1b0fb4d264ca75ac59b33ea2eab4e1234 100644 (file)
--- 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] ≝