From 8a2b0d520b7863694130de56c5bf30fdd07696bd Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 2 Mar 2010 16:39:15 +0000 Subject: [PATCH] Added reverse rewriting principle in Type[0]. --- helm/software/matita/nlibrary/logic/equality.ma | 11 +++++++++++ 1 file changed, 11 insertions(+) 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] ≝ -- 2.39.2