legacy_1, ground_1, and basic_1 recommitted without anticipation

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / lift / tlt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
index 1d8edc7df1ade777f0dce10e9bc7b0b1e35bc855..d66d095ef9004493d2fdaa6c81f3ac19dbbbaa5e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/lift/fwd.ma".
+include "basic_1/lift/props.ma".
 
-include "Basic-1/tlt/props.ma".
+include "basic_1/tlt/props.ma".
 
 theorem lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to 
@@ -105,9 +105,6 @@ t0)) (weight_map f (lift h d t1))) (plus (weight_map f t0) (weight_map f t1))
 (weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1))) 
 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) 
 k)))))))))) t).
-(* COMMENTS
-Initial nodes: 1969
-END *)
 
 theorem lift_weight:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(eq nat (weight (lift h d 
@@ -116,9 +113,6 @@ t)) (weight t))))
  \lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d 
 (\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat 
 O)))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
 
 theorem lift_weight_add:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d: 
@@ -267,9 +261,6 @@ t0)) (weight_map f (lift h d t1))) (plus (weight_map g (lift (S h) d t0))
 (lift (S h) d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 (S h) d)) 
 (lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) 
 k))))))))))))) t)).
-(* COMMENTS
-Initial nodes: 3697
-END *)
 
 theorem lift_weight_add_O:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to 
@@ -277,13 +268,10 @@ nat))).(eq nat (weight_map f (lift h O t)) (weight_map (wadd f w) (lift (S h)
 O t))))))
 \def
  \lambda (w: nat).(\lambda (t: T).(\lambda (h: nat).(\lambda (f: ((nat \to 
-nat))).(lift_weight_add (plus (wadd f w O) O) t h O f (wadd f w) (\lambda (m: 
-nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m))))) 
-(plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal 
+nat))).(lift_weight_add (minus (wadd f w O) O) t h O f (wadd f w) (\lambda 
+(m: nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m))))) 
+(minus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal 
 nat (f m)))))))).
-(* COMMENTS
-Initial nodes: 93
-END *)
 
 theorem lift_tlt_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall 
@@ -293,7 +281,4 @@ theorem lift_tlt_dx:
 (d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight 
 (THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t) 
 (lift_weight t h d)))))).
-(* COMMENTS
-Initial nodes: 71
-END *)