- some new auxiliary lemmas

[helm.git] / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / subst0 / tlt.ma

diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma
index 37b74c00cb0adc6020dbbb4cd26730d14a747476..fd0ba2f0cb9cc041190467f15843f715f0c8af50 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma
+++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma
@@ -75,35 +75,33 @@ u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
 f g H2 O O (le_n O) n))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to 
 nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 
 m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g 
-i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t0)) (S (plus 
-(weight_map g u1) (weight_map g t0))) (le_lt_n_Sm (plus (weight_map f0 u2) 
-(weight_map f0 t0)) (plus (weight_map g u1) (weight_map g t0)) 
-(plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t0) 
-(weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g H2))))))))) k))))))))) 
-(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v: T).(\forall (t2: 
-T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1 t2) \to 
-(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
-nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s 
-k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: 
-T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
-nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to 
-(le (weight_map f (THead k0 u0 t2)) (weight_map g (THead k0 u0 
-t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda (b0: B).(\forall (v: 
-T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s (Bind b0) 
-i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
+i))).(le_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g 
+u1) (weight_map g t0)) (plus_le_compat (weight_map f0 u2) (weight_map g u1) 
+(weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g 
+H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v: 
+T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1 
+t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
-(s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2) 
-(weight_map g t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to 
-nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
-\to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead 
-(Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0 t1))))))))))))))) 
-(\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda 
-(_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to 
+(s k0 i)) O v)) (g (s k0 i))) \to (le (weight_map f t2) (weight_map g 
+t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g: 
+((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map 
+f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead k0 u0 t2)) 
+(weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda 
+(b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i: 
+nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to 
 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
-\to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f 
-t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to 
-nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f 
-m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
+\to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) 
+\to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: 
+T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
+nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to 
+(le (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0 
+t1))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda 
+(i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: 
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
+(g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le 
+(weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: 
+((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: 
+nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
 i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f (S (weight_map f 
 u0))) t2)) (plus (weight_map g u0) (weight_map (wadd g (S (weight_map g u0))) 
 t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f 
@@ -111,25 +109,24 @@ t1)) (plus_le_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd f
 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S 
 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0)) 
 (S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le 
-u0 f g H2)) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S 
-(S i)) O v)) (wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f 
-(lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S 
-(weight_map f u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f 
-u0)) v (S i) f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda 
-(t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: 
-((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
-nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S 
-i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: 
-T).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: 
-((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift 
-(S i) O v)) (g i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f O) 
-t2)) (plus (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_compat 
-(weight_map f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map 
-(wadd g O) t1) (weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: 
-nat).(wadd_le f g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O 
-v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) 
-O v)) (lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda 
-(t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1 
+u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: 
+nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S 
+i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f)))))))))))))))) 
+(\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda 
+(_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
+\to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f 
+t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to 
+nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f 
+m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
+i))).(le_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus 
+(weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_compat (weight_map f 
+u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) 
+(weight_le u0 f g H2) (H1 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f 
+g H2 O O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda 
+(n: nat).(lt n (g i))) H3 (weight_map (wadd f O) (lift (S (S i)) O v)) 
+(lift_weight_add_O O v (S i) f)))))))))))))))) (\lambda (v: T).(\lambda (t2: 
+T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (_: (subst0 (S i) v t1 
 t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
 nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
 (S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g 
@@ -149,30 +146,29 @@ nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
 (S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g 
 t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat 
 \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda 
-(H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_le_S (plus (weight_map 
-f0 u0) (weight_map f0 t2)) (S (plus (weight_map g u0) (weight_map g t1))) 
-(le_lt_n_Sm (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g 
-u0) (weight_map g t1)) (plus_le_compat (weight_map f0 u0) (weight_map g u0) 
-(weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 
-H3)))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2: 
-T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall 
-(f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f 
-m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le 
-(weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda 
-(k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to 
-(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
-nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s 
-k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f: 
-((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
-(g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map 
-f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: 
-B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s 
-(Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat 
+(H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map 
+f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g t1)) 
+(plus_le_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2) 
+(weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3))))))))))))))) k)) 
+(\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda 
+(_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall 
+(g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt 
+(weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f u2) (weight_map 
+g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1: 
+T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
+\to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (le 
+(weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
+\to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead 
+k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind 
+(\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v 
+t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
+nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
+(s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2) 
+(weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat 
 \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f 
-(lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f 
-t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: 
-((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map 
-f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2)) 
+(lift (S i) O v)) (g i)) \to (le (weight_map f (THead (Bind b0) u2 t2)) 
 (weight_map g (THead (Bind b0) u1 t1)))))))))))) (\lambda (t1: T).(\lambda 
 (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: 
 ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
@@ -186,25 +182,11 @@ t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f
 (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) (H1 
 f g H4 H5) (H3 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map g u1))) 
 (\lambda (m: nat).(wadd_le f g H4 (S (weight_map f u2)) (S (weight_map g u1)) 
-(le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (lt_le_S 
-(weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v)) (wadd g (S 
-(weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S i) O v)) 
-(\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f u2))) 
-(lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i) 
-f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) 
-v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
-nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
-(S i)) O v)) (g (S i))) \to (le (weight_map f t2) (weight_map g 
-t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
-nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt 
-(weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2) 
-(weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O) 
-t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f 
-O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) 
-(\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f 
-(lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) 
-(lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda 
-(t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: 
+(le_n_S (weight_map f u2) (weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat 
+(weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 
+(weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) O v)) 
+(lift_weight_add_O (S (weight_map f u2)) v (S i) f))))))))))))) (\lambda (t1: 
+T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: 
 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S 
 i))) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat 
@@ -216,18 +198,29 @@ u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(wadd_le f g H4 O 
 O (le_n O) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: 
 nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) 
-(lift_weight_add_O O v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: 
-T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall 
-(f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le 
-(f0 m) (g m)))) \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (le 
-(weight_map f0 t2) (weight_map g t1)))))))).(\lambda (f0: ((nat \to 
-nat))).(\lambda (g: ((nat \to nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 
-m) (g m))))).(\lambda (H5: (lt (weight_map f0 (lift (S i) O v)) (g 
-i))).(lt_le_S (plus (weight_map f0 u2) (weight_map f0 t2)) (S (plus 
-(weight_map g u1) (weight_map g t1))) (le_lt_n_Sm (plus (weight_map f0 u2) 
+(lift_weight_add_O O v (S i) f))))))))))))) (\lambda (t1: T).(\lambda (t2: 
+T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
+\to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (le (weight_map f 
+t2) (weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat 
+\to nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: 
+(lt (weight_map f (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f u2) 
+(weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O) 
+t1)) (plus_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f 
+O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) 
+(\lambda (m: nat).(wadd_le f g H4 O O (le_n O) m)) (eq_ind nat (weight_map f 
+(lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) 
+(lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) b)) 
+(\lambda (_: F).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 i v t1 
+t2)).(\lambda (H3: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to 
+nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift 
+(S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g 
+t1)))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to 
+nat))).(\lambda (H4: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H5: 
+(lt (weight_map f0 (lift (S i) O v)) (g i))).(le_n_S (plus (weight_map f0 u2) 
 (weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1)) 
 (plus_le_compat (weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) 
-(weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5))))))))))))) k)))))))) d u t 
+(weight_map g t1) (H1 f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t 
 z H))))).
 
 theorem subst0_weight_lt:
@@ -263,9 +256,16 @@ m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g i))).(lt_n_S
 (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f (S 
 (weight_map f u2))) t0) (weight_map (wadd g (S (weight_map g u1))) t0) (H1 f 
 g H2 H3) (weight_le t0 (wadd f (S (weight_map f u2))) (wadd g (S (weight_map 
-g u1))) (\lambda (n: nat).(wadd_le f g H2 (S (weight_map f u2)) (S 
-(weight_map g u1)) (le_S (S (weight_map f u2)) (weight_map g u1) (lt_le_S 
-(weight_map f u2) (weight_map g u1) (H1 f g H2 H3))) n))))))))) (\lambda (f: 
+g u1))) (\lambda (n: nat).(wadd_lt f g H2 (S (weight_map f u2)) (S 
+(weight_map g u1)) (lt_n_S (weight_map f u2) (weight_map g u1) (H1 f g H2 
+H3)) n))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
+nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt 
+(weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2) 
+(weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O) 
+t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd 
+f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O) 
+(wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd 
+f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) (\lambda (f: 
 ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: 
 nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
 i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus 
@@ -273,33 +273,26 @@ i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t0)) (plus
 f u2) (weight_map g u1) (weight_map (wadd f O) t0) (weight_map (wadd g O) t0) 
 (H1 f g H2 H3) (weight_le t0 (wadd f O) (wadd g O) (\lambda (n: nat).(le_S_n 
 (wadd f O n) (wadd g O n) (le_n_S (wadd f O n) (wadd g O n) (wadd_le f g H2 O 
-O (le_n O) n))))))))))) (\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
-nat))).(\lambda (H2: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H3: (lt 
-(weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2) 
-(weight_map (wadd f O) t0)) (plus (weight_map g u1) (weight_map (wadd g O) 
-t0)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd 
-f O) t0) (weight_map (wadd g O) t0) (H1 f g H2 H3) (weight_le t0 (wadd f O) 
-(wadd g O) (\lambda (n: nat).(le_S_n (wadd f O n) (wadd g O n) (le_n_S (wadd 
-f O n) (wadd g O n) (wadd_le f g H2 O O (le_n O) n))))))))))) b)) (\lambda 
-(_: F).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda 
-(H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H3: (lt (weight_map f0 
-(lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 
-t0)) (plus (weight_map g u1) (weight_map g t0)) (plus_lt_le_compat 
-(weight_map f0 u2) (weight_map g u1) (weight_map f0 t0) (weight_map g t0) (H1 
-f0 g H2 H3) (weight_le t0 f0 g H2)))))))) k))))))))) (\lambda (k: K).(K_ind 
-(\lambda (k0: K).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall 
-(i: nat).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to 
+O (le_n O) n))))))))))) b)) (\lambda (_: F).(\lambda (f0: ((nat \to 
+nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 
+m) (g m))))).(\lambda (H3: (lt (weight_map f0 (lift (S i) O v)) (g 
+i))).(lt_n_S (plus (weight_map f0 u2) (weight_map f0 t0)) (plus (weight_map g 
+u1) (weight_map g t0)) (plus_lt_le_compat (weight_map f0 u2) (weight_map g 
+u1) (weight_map f0 t0) (weight_map g t0) (H1 f0 g H2 H3) (weight_le t0 f0 g 
+H2)))))))) k))))))))) (\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (v: 
+T).(\forall (t2: T).(\forall (t1: T).(\forall (i: nat).((subst0 (s k0 i) v t1 
+t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
+nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
+(s k0 i)) O v)) (g (s k0 i))) \to (lt (weight_map f t2) (weight_map g 
+t1))))))) \to (\forall (u0: T).(\forall (f: ((nat \to nat))).(\forall (g: 
+((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map 
+f (lift (S i) O v)) (g i)) \to (lt (weight_map f (THead k0 u0 t2)) 
+(weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: B).(B_ind (\lambda 
+(b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: T).(\forall (i: 
+nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to 
 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
-\to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (lt 
-(weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: T).(\forall (f: 
-((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
-(g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (lt (weight_map 
-f (THead k0 u0 t2)) (weight_map g (THead k0 u0 t1))))))))))))))) (\lambda (b: 
-B).(B_ind (\lambda (b0: B).(\forall (v: T).(\forall (t2: T).(\forall (t1: 
-T).(\forall (i: nat).((subst0 (s (Bind b0) i) v t1 t2) \to (((\forall (f: 
-((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
-(g m)))) \to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind 
-b0) i))) \to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: 
+\to ((lt (weight_map f (lift (S (s (Bind b0) i)) O v)) (g (s (Bind b0) i))) 
+\to (lt (weight_map f t2) (weight_map g t1))))))) \to (\forall (u0: 
 T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to 
 (lt (weight_map f (THead (Bind b0) u0 t2)) (weight_map g (THead (Bind b0) u0 
@@ -316,19 +309,17 @@ t1)) (plus_le_lt_compat (weight_map f u0) (weight_map g u0) (weight_map (wadd
 f (S (weight_map f u0))) t2) (weight_map (wadd g (S (weight_map g u0))) t1) 
 (weight_le u0 f g H2) (H1 (wadd f (S (weight_map f u0))) (wadd g (S 
 (weight_map g u0))) (\lambda (m: nat).(wadd_le f g H2 (S (weight_map f u0)) 
-(S (weight_map g u0)) (lt_le_S (weight_map f u0) (S (weight_map g u0)) 
-(le_lt_n_Sm (weight_map f u0) (weight_map g u0) (weight_le u0 f g H2))) m)) 
-(lt_le_S (weight_map (wadd f (S (weight_map f u0))) (lift (S (S i)) O v)) 
-(wadd g (S (weight_map g u0)) (S i)) (eq_ind nat (weight_map f (lift (S i) O 
-v)) (\lambda (n: nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f 
-u0))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) 
-f))))))))))))))))) (\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda 
-(i: nat).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: 
-((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) 
-(g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt 
-(weight_map f t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: 
-((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: 
-nat).(le (f m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
+(S (weight_map g u0)) (le_n_S (weight_map f u0) (weight_map g u0) (weight_le 
+u0 f g H2)) m)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: 
+nat).(lt n (g i))) H3 (weight_map (wadd f (S (weight_map f u0))) (lift (S (S 
+i)) O v)) (lift_weight_add_O (S (weight_map f u0)) v (S i) f)))))))))))))))) 
+(\lambda (v: T).(\lambda (t2: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda 
+(_: (subst0 (S i) v t1 t2)).(\lambda (H1: ((\forall (f: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) 
+\to ((lt (weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f 
+t2) (weight_map g t1)))))))).(\lambda (u0: T).(\lambda (f: ((nat \to 
+nat))).(\lambda (g: ((nat \to nat))).(\lambda (H2: ((\forall (m: nat).(le (f 
+m) (g m))))).(\lambda (H3: (lt (weight_map f (lift (S i) O v)) (g 
 i))).(lt_n_S (plus (weight_map f u0) (weight_map (wadd f O) t2)) (plus 
 (weight_map g u0) (weight_map (wadd g O) t1)) (plus_le_lt_compat (weight_map 
 f u0) (weight_map g u0) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) 
@@ -391,29 +382,26 @@ u2))) t2)) (plus (weight_map g u1) (weight_map (wadd g (S (weight_map g u1)))
 t1)) (plus_lt_le_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd 
 f (S (weight_map f u2))) t2) (weight_map (wadd g (S (weight_map g u1))) t1) 
 (H1 f g H4 H5) (subst0_weight_le v t1 t2 (S i) H2 (wadd f (S (weight_map f 
-u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_le f g H4 (S 
-(weight_map f u2)) (S (weight_map g u1)) (le_S (S (weight_map f u2)) 
-(weight_map g u1) (lt_le_S (weight_map f u2) (weight_map g u1) (H1 f g H4 
-H5))) m)) (lt_le_S (weight_map (wadd f (S (weight_map f u2))) (lift (S (S i)) 
-O v)) (wadd g (S (weight_map g u1)) (S i)) (eq_ind nat (weight_map f (lift (S 
-i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S 
-(weight_map f u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f 
-u2)) v (S i) f)))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: 
-(subst0 (S i) v t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall 
-(g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt 
-(weight_map f (lift (S (S i)) O v)) (g (S i))) \to (lt (weight_map f t2) 
-(weight_map g t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
+u2))) (wadd g (S (weight_map g u1))) (\lambda (m: nat).(wadd_lt f g H4 (S 
+(weight_map f u2)) (S (weight_map g u1)) (lt_n_S (weight_map f u2) 
+(weight_map g u1) (H1 f g H4 H5)) m)) (eq_ind nat (weight_map f (lift (S i) O 
+v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f (S (weight_map f 
+u2))) (lift (S (S i)) O v)) (lift_weight_add_O (S (weight_map f u2)) v (S i) 
+f))))))))))))) (\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v 
+t1 t2)).(\lambda (H3: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to 
+nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S 
+(S i)) O v)) (g (S i))) \to (lt (weight_map f t2) (weight_map g 
+t1)))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
 nat))).(\lambda (H4: ((\forall (m: nat).(le (f m) (g m))))).(\lambda (H5: (lt 
 (weight_map f (lift (S i) O v)) (g i))).(lt_n_S (plus (weight_map f u2) 
 (weight_map (wadd f O) t2)) (plus (weight_map g u1) (weight_map (wadd g O) 
 t1)) (plus_lt_compat (weight_map f u2) (weight_map g u1) (weight_map (wadd f 
 O) t2) (weight_map (wadd g O) t1) (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) 
 (\lambda (m: nat).(le_S_n (wadd f O m) (wadd g O m) (le_n_S (wadd f O m) 
-(wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (lt_le_S (weight_map (wadd f 
-O) (lift (S (S i)) O v)) (wadd g O (S i)) (eq_ind nat (weight_map f (lift (S 
-i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) (lift (S 
-(S i)) O v)) (lift_weight_add_O O v (S i) f)))))))))))))) (\lambda (t1: 
-T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: 
+(wadd g O m) (wadd_le f g H4 O O (le_n O) m)))) (eq_ind nat (weight_map f 
+(lift (S i) O v)) (\lambda (n: nat).(lt n (g i))) H5 (weight_map (wadd f O) 
+(lift (S (S i)) O v)) (lift_weight_add_O O v (S i) f))))))))))))) (\lambda 
+(t1: T).(\lambda (t2: T).(\lambda (_: (subst0 (S i) v t1 t2)).(\lambda (H3: 
 ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: 
 nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (S i)) O v)) (g (S 
 i))) \to (lt (weight_map f t2) (weight_map g t1)))))))).(\lambda (f: ((nat 
@@ -424,10 +412,9 @@ i))).(lt_n_S (plus (weight_map f u2) (weight_map (wadd f O) t2)) (plus
 u2) (weight_map g u1) (weight_map (wadd f O) t2) (weight_map (wadd g O) t1) 
 (H1 f g H4 H5) (H3 (wadd f O) (wadd g O) (\lambda (m: nat).(le_S_n (wadd f O 
 m) (wadd g O m) (le_n_S (wadd f O m) (wadd g O m) (wadd_le f g H4 O O (le_n 
-O) m)))) (lt_le_S (weight_map (wadd f O) (lift (S (S i)) O v)) (wadd g O (S 
-i)) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n (g 
-i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O v 
-(S i) f)))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: 
+O) m)))) (eq_ind nat (weight_map f (lift (S i) O v)) (\lambda (n: nat).(lt n 
+(g i))) H5 (weight_map (wadd f O) (lift (S (S i)) O v)) (lift_weight_add_O O 
+v (S i) f))))))))))))) b)) (\lambda (_: F).(\lambda (t1: T).(\lambda (t2: 
 T).(\lambda (_: (subst0 i v t1 t2)).(\lambda (H3: ((\forall (f0: ((nat \to 
 nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f0 m) (g m)))) 
 \to ((lt (weight_map f0 (lift (S i) O v)) (g i)) \to (lt (weight_map f0 t2)