X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Flift%2Fprops.ma;h=748f9a280b31209a7be85f794186137318e63cdc;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=20649f9bf4357b641e5c0495d29814207c967d4d;hpb=eccaad18aa815bb3334e205b97c220f675e6d5a5;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
index 20649f9bf..748f9a280 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
@@ -379,6 +379,55 @@ H11) x1 H10)))) (H0 x1 h1 h2 d1 d2 H1 H7)) t H9) x0 H8)))) (H x0 h1 h2 d1 d2
 H1 H6)) x H5)))))) (lift_gen_flat f (lift h1 d1 t) (lift h1 d1 t0) x h2 (plus 
 d2 h1) H4))))) k H2))))))))))))) t1).
 
+theorem lifts_inj:
+ \forall (xs: TList).(\forall (ts: TList).(\forall (h: nat).(\forall (d: 
+nat).((eq TList (lifts h d xs) (lifts h d ts)) \to (eq TList xs ts)))))
+\def
+ \lambda (xs: TList).(TList_ind (\lambda (t: TList).(\forall (ts: 
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d t) (lifts h 
+d ts)) \to (eq TList t ts)))))) (\lambda (ts: TList).(TList_ind (\lambda (t: 
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d TNil) (lifts 
+h d t)) \to (eq TList TNil t))))) (\lambda (_: nat).(\lambda (_: 
+nat).(\lambda (_: (eq TList TNil TNil)).(refl_equal TList TNil)))) (\lambda 
+(t: T).(\lambda (t0: TList).(\lambda (_: ((\forall (h: nat).(\forall (d: 
+nat).((eq TList TNil (lifts h d t0)) \to (eq TList TNil t0)))))).(\lambda (h: 
+nat).(\lambda (d: nat).(\lambda (H0: (eq TList TNil (TCons (lift h d t) 
+(lifts h d t0)))).(let H1 \def (eq_ind TList TNil (\lambda (ee: TList).(match 
+ee in TList return (\lambda (_: TList).Prop) with [TNil \Rightarrow True | 
+(TCons _ _) \Rightarrow False])) I (TCons (lift h d t) (lifts h d t0)) H0) in 
+(False_ind (eq TList TNil (TCons t t0)) H1)))))))) ts)) (\lambda (t: 
+T).(\lambda (t0: TList).(\lambda (H: ((\forall (ts: TList).(\forall (h: 
+nat).(\forall (d: nat).((eq TList (lifts h d t0) (lifts h d ts)) \to (eq 
+TList t0 ts))))))).(\lambda (ts: TList).(TList_ind (\lambda (t1: 
+TList).(\forall (h: nat).(\forall (d: nat).((eq TList (lifts h d (TCons t 
+t0)) (lifts h d t1)) \to (eq TList (TCons t t0) t1))))) (\lambda (h: 
+nat).(\lambda (d: nat).(\lambda (H0: (eq TList (TCons (lift h d t) (lifts h d 
+t0)) TNil)).(let H1 \def (eq_ind TList (TCons (lift h d t) (lifts h d t0)) 
+(\lambda (ee: TList).(match ee in TList return (\lambda (_: TList).Prop) with 
+[TNil \Rightarrow False | (TCons _ _) \Rightarrow True])) I TNil H0) in 
+(False_ind (eq TList (TCons t t0) TNil) H1))))) (\lambda (t1: T).(\lambda 
+(t2: TList).(\lambda (_: ((\forall (h: nat).(\forall (d: nat).((eq TList 
+(TCons (lift h d t) (lifts h d t0)) (lifts h d t2)) \to (eq TList (TCons t 
+t0) t2)))))).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (eq TList 
+(TCons (lift h d t) (lifts h d t0)) (TCons (lift h d t1) (lifts h d 
+t2)))).(let H2 \def (f_equal TList T (\lambda (e: TList).(match e in TList 
+return (\lambda (_: TList).T) with [TNil \Rightarrow ((let rec lref_map (f: 
+((nat \to nat))) (d0: nat) (t3: T) on t3: T \def (match t3 with [(TSort n) 
+\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0) with 
+[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t4) \Rightarrow 
+(THead k (lref_map f d0 u) (lref_map f (s k d0) t4))]) in lref_map) (\lambda 
+(x: nat).(plus x h)) d t) | (TCons t3 _) \Rightarrow t3])) (TCons (lift h d 
+t) (lifts h d t0)) (TCons (lift h d t1) (lifts h d t2)) H1) in ((let H3 \def 
+(f_equal TList TList (\lambda (e: TList).(match e in TList return (\lambda 
+(_: TList).TList) with [TNil \Rightarrow ((let rec lifts (h0: nat) (d0: nat) 
+(ts0: TList) on ts0: TList \def (match ts0 with [TNil \Rightarrow TNil | 
+(TCons t3 ts1) \Rightarrow (TCons (lift h0 d0 t3) (lifts h0 d0 ts1))]) in 
+lifts) h d t0) | (TCons _ t3) \Rightarrow t3])) (TCons (lift h d t) (lifts h 
+d t0)) (TCons (lift h d t1) (lifts h d t2)) H1) in (\lambda (H4: (eq T (lift 
+h d t) (lift h d t1))).(eq_ind T t (\lambda (t3: T).(eq TList (TCons t t0) 
+(TCons t3 t2))) (f_equal2 T TList TList TCons t t t0 t2 (refl_equal T t) (H 
+t2 h d H3)) t1 (lift_inj t t1 h d H4)))) H2)))))))) ts))))) xs).
+
 theorem lift_free:
  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: 
 nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to (eq T (lift k e