X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Flift%2Fprops.ma;h=f0ed224515471af542b1c2c07e16cd6056cb3e4f;hb=d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a;hp=748f9a280b31209a7be85f794186137318e63cdc;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/props.ma
index 748f9a280..f0ed22451 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/lift/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/lift/fwd.ma".
+include "Basic-1/lift/fwd.ma".
 
-include "LambdaDelta-1/s/props.ma".
+include "Basic-1/s/props.ma".
 
 theorem thead_x_lift_y_y:
  \forall (k: K).(\forall (t: T).(\forall (v: T).(\forall (h: nat).(\forall 
@@ -78,6 +78,9 @@ Prop).P0)))))) H0 k0 H6) in (let H8 \def (eq_ind T (lift h d (THead k0 t0
 t1)) (\lambda (t2: T).(eq T t2 t1)) H4 (THead k0 (lift h d t0) (lift h (s k0 
 d) t1)) (lift_head k0 t0 t1 h d)) in (H7 (lift h d t0) h (s k0 d) H8 P)))))) 
 H3)) H2)))))))))))) t)).
+(* COMMENTS
+Initial nodes: 887
+END *)
 
 theorem lift_r:
  \forall (t: T).(\forall (d: nat).(eq T (lift O d t) t))
@@ -96,6 +99,9 @@ t1)))).(\lambda (d: nat).(eq_ind_r T (THead k (lift O d t0) (lift O (s k d)
 t1)) (\lambda (t2: T).(eq T t2 (THead k t0 t1))) (f_equal3 K T T T THead k k 
 (lift O d t0) t0 (lift O (s k d) t1) t1 (refl_equal K k) (H d) (H0 (s k d))) 
 (lift O d (THead k t0 t1)) (lift_head k t0 t1 O d)))))))) t).
+(* COMMENTS
+Initial nodes: 367
+END *)
 
 theorem lift_lref_gt:
  \forall (d: nat).(\forall (n: nat).((lt d n) \to (eq T (lift (S O) d (TLRef 
@@ -109,6 +115,9 @@ theorem lift_lref_gt:
 (lift (S O) d (TLRef (pred n))) (lift_lref_ge (pred n) (S O) d (le_S_n d 
 (pred n) (eq_ind nat n (\lambda (n0: nat).(le (S d) n0)) H (S (pred n)) 
 (S_pred n d H))))))).
+(* COMMENTS
+Initial nodes: 193
+END *)
 
 theorem lifts_tapp:
  \forall (h: nat).(\forall (d: nat).(\forall (v: T).(\forall (vs: TList).(eq 
@@ -123,6 +132,9 @@ t0) (lift h d v)) (\lambda (t1: TList).(eq TList (TCons (lift h d t) t1)
 (TCons (lift h d t) (TApp (lifts h d t0) (lift h d v))))) (refl_equal TList 
 (TCons (lift h d t) (TApp (lifts h d t0) (lift h d v)))) (lifts h d (TApp t0 
 v)) H)))) vs)))).
+(* COMMENTS
+Initial nodes: 215
+END *)
 
 theorem lift_inj:
  \forall (x: T).(\forall (t: T).(\forall (h: nat).(\forall (d: nat).((eq T 
@@ -183,6 +195,9 @@ T).(\lambda (x1: T).(\lambda (H3: (eq T t1 (THead (Flat f) x0 x1))).(\lambda
 (THead (Flat f) t t0) t2)) (f_equal3 K T T T THead (Flat f) (Flat f) t x0 t0 
 x1 (refl_equal K (Flat f)) (H x0 h d H4) (H0 x1 h d H5)) t1 H3)))))) 
 (lift_gen_flat f (lift h d t) (lift h d t0) t1 h d H2)))))))))))) k)) x).
+(* COMMENTS
+Initial nodes: 1391
+END *)
 
 theorem lift_gen_lift:
  \forall (t1: T).(\forall (x: T).(\forall (h1: nat).(\forall (h2: 
@@ -378,6 +393,9 @@ d2 x3))) (lift h2 d2 (THead (Flat f) x2 x3)) (lift_flat f x2 x3 h2 d2))) t0
 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).
+(* COMMENTS
+Initial nodes: 5037
+END *)
 
 theorem lifts_inj:
  \forall (xs: TList).(\forall (ts: TList).(\forall (h: nat).(\forall (d: 
@@ -427,6 +445,9 @@ 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).
+(* COMMENTS
+Initial nodes: 772
+END *)
 
 theorem lift_free:
  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: 
@@ -484,6 +505,9 @@ k e (plus d h) H1) (plus (s k d) h) (s_plus k d h)) (s_le k d e H2))) (lift
 (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k (lift h d t0) (lift 
 h (s k d) t1) k0 e)) (lift h d (THead k t0 t1)) (lift_head k t0 t1 h 
 d))))))))))))) t).
+(* COMMENTS
+Initial nodes: 1407
+END *)
 
 theorem lift_d:
  \forall (t: T).(\forall (h: nat).(\forall (k: nat).(\forall (d: 
@@ -562,4 +586,7 @@ d)) (lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))) (lift_head k
 (lift_head k t0 t1 h d)) (lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0 
 (s k e) t1))) (lift_head k (lift k0 e t0) (lift k0 (s k e) t1) h (plus k0 
 d))) (lift k0 e (THead k t0 t1)) (lift_head k t0 t1 k0 e)))))))))))) t).
+(* COMMENTS
+Initial nodes: 2143
+END *)