-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)) (le_plus_plus (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: ((\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)) (le_plus_plus (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)) (le_plus_plus
-(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 z H))))).
-(* COMMENTS
-Initial nodes: 4101
-END *)
+i))).(let TMP_315 \def (weight_map f u2) in (let TMP_316 \def (weight_map f
+u2) in (let TMP_317 \def (S TMP_316) in (let TMP_318 \def (wadd f TMP_317) in
+(let TMP_319 \def (weight_map TMP_318 t2) in (let TMP_320 \def (plus TMP_315
+TMP_319) in (let TMP_321 \def (weight_map g u1) in (let TMP_322 \def
+(weight_map g u1) in (let TMP_323 \def (S TMP_322) in (let TMP_324 \def (wadd
+g TMP_323) in (let TMP_325 \def (weight_map TMP_324 t1) in (let TMP_326 \def
+(plus TMP_321 TMP_325) in (let TMP_327 \def (weight_map f u2) in (let TMP_328
+\def (weight_map g u1) in (let TMP_329 \def (weight_map f u2) in (let TMP_330
+\def (S TMP_329) in (let TMP_331 \def (wadd f TMP_330) in (let TMP_332 \def
+(weight_map TMP_331 t2) in (let TMP_333 \def (weight_map g u1) in (let
+TMP_334 \def (S TMP_333) in (let TMP_335 \def (wadd g TMP_334) in (let
+TMP_336 \def (weight_map TMP_335 t1) in (let TMP_337 \def (H1 f g H4 H5) in
+(let TMP_338 \def (weight_map f u2) in (let TMP_339 \def (S TMP_338) in (let
+TMP_340 \def (wadd f TMP_339) in (let TMP_341 \def (weight_map g u1) in (let
+TMP_342 \def (S TMP_341) in (let TMP_343 \def (wadd g TMP_342) in (let
+TMP_352 \def (\lambda (m: nat).(let TMP_344 \def (weight_map f u2) in (let
+TMP_345 \def (S TMP_344) in (let TMP_346 \def (weight_map g u1) in (let
+TMP_347 \def (S TMP_346) in (let TMP_348 \def (weight_map f u2) in (let
+TMP_349 \def (weight_map g u1) in (let TMP_350 \def (H1 f g H4 H5) in (let
+TMP_351 \def (le_n_S TMP_348 TMP_349 TMP_350) in (wadd_le f g H4 TMP_345
+TMP_347 TMP_351 m)))))))))) in (let TMP_353 \def (S i) in (let TMP_354 \def
+(lift TMP_353 O v) in (let TMP_355 \def (weight_map f TMP_354) in (let
+TMP_357 \def (\lambda (n: nat).(let TMP_356 \def (g i) in (lt n TMP_356))) in
+(let TMP_358 \def (weight_map f u2) in (let TMP_359 \def (S TMP_358) in (let
+TMP_360 \def (wadd f TMP_359) in (let TMP_361 \def (S i) in (let TMP_362 \def
+(S TMP_361) in (let TMP_363 \def (lift TMP_362 O v) in (let TMP_364 \def
+(weight_map TMP_360 TMP_363) in (let TMP_365 \def (weight_map f u2) in (let
+TMP_366 \def (S TMP_365) in (let TMP_367 \def (S i) in (let TMP_368 \def
+(lift_weight_add_O TMP_366 v TMP_367 f) in (let TMP_369 \def (eq_ind nat
+TMP_355 TMP_357 H5 TMP_364 TMP_368) in (let TMP_370 \def (H3 TMP_340 TMP_343
+TMP_352 TMP_369) in (let TMP_371 \def (le_plus_plus TMP_327 TMP_328 TMP_332
+TMP_336 TMP_337 TMP_370) in (le_n_S TMP_320 TMP_326
+TMP_371))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let
+TMP_407 \def (\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))).(let TMP_373 \def (weight_map f u2)
+in (let TMP_374 \def (wadd f O) in (let TMP_375 \def (weight_map TMP_374 t2)
+in (let TMP_376 \def (plus TMP_373 TMP_375) in (let TMP_377 \def (weight_map
+g u1) in (let TMP_378 \def (wadd g O) in (let TMP_379 \def (weight_map
+TMP_378 t1) in (let TMP_380 \def (plus TMP_377 TMP_379) in (let TMP_381 \def
+(weight_map f u2) in (let TMP_382 \def (weight_map g u1) in (let TMP_383 \def
+(wadd f O) in (let TMP_384 \def (weight_map TMP_383 t2) in (let TMP_385 \def
+(wadd g O) in (let TMP_386 \def (weight_map TMP_385 t1) in (let TMP_387 \def
+(H1 f g H4 H5) in (let TMP_388 \def (wadd f O) in (let TMP_389 \def (wadd g
+O) in (let TMP_391 \def (\lambda (m: nat).(let TMP_390 \def (le_O_n O) in
+(wadd_le f g H4 O O TMP_390 m))) in (let TMP_392 \def (S i) in (let TMP_393
+\def (lift TMP_392 O v) in (let TMP_394 \def (weight_map f TMP_393) in (let
+TMP_396 \def (\lambda (n: nat).(let TMP_395 \def (g i) in (lt n TMP_395))) in
+(let TMP_397 \def (wadd f O) in (let TMP_398 \def (S i) in (let TMP_399 \def
+(S TMP_398) in (let TMP_400 \def (lift TMP_399 O v) in (let TMP_401 \def
+(weight_map TMP_397 TMP_400) in (let TMP_402 \def (S i) in (let TMP_403 \def
+(lift_weight_add_O O v TMP_402 f) in (let TMP_404 \def (eq_ind nat TMP_394
+TMP_396 H5 TMP_401 TMP_403) in (let TMP_405 \def (H3 TMP_388 TMP_389 TMP_391
+TMP_404) in (let TMP_406 \def (le_plus_plus TMP_381 TMP_382 TMP_384 TMP_386
+TMP_387 TMP_405) in (le_n_S TMP_376 TMP_380
+TMP_406))))))))))))))))))))))))))))))))))))))))) in (let TMP_442 \def
+(\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))).(let TMP_408 \def (weight_map f u2)
+in (let TMP_409 \def (wadd f O) in (let TMP_410 \def (weight_map TMP_409 t2)
+in (let TMP_411 \def (plus TMP_408 TMP_410) in (let TMP_412 \def (weight_map
+g u1) in (let TMP_413 \def (wadd g O) in (let TMP_414 \def (weight_map
+TMP_413 t1) in (let TMP_415 \def (plus TMP_412 TMP_414) in (let TMP_416 \def
+(weight_map f u2) in (let TMP_417 \def (weight_map g u1) in (let TMP_418 \def
+(wadd f O) in (let TMP_419 \def (weight_map TMP_418 t2) in (let TMP_420 \def
+(wadd g O) in (let TMP_421 \def (weight_map TMP_420 t1) in (let TMP_422 \def
+(H1 f g H4 H5) in (let TMP_423 \def (wadd f O) in (let TMP_424 \def (wadd g
+O) in (let TMP_426 \def (\lambda (m: nat).(let TMP_425 \def (le_O_n O) in
+(wadd_le f g H4 O O TMP_425 m))) in (let TMP_427 \def (S i) in (let TMP_428
+\def (lift TMP_427 O v) in (let TMP_429 \def (weight_map f TMP_428) in (let
+TMP_431 \def (\lambda (n: nat).(let TMP_430 \def (g i) in (lt n TMP_430))) in
+(let TMP_432 \def (wadd f O) in (let TMP_433 \def (S i) in (let TMP_434 \def
+(S TMP_433) in (let TMP_435 \def (lift TMP_434 O v) in (let TMP_436 \def
+(weight_map TMP_432 TMP_435) in (let TMP_437 \def (S i) in (let TMP_438 \def
+(lift_weight_add_O O v TMP_437 f) in (let TMP_439 \def (eq_ind nat TMP_429
+TMP_431 H5 TMP_436 TMP_438) in (let TMP_440 \def (H3 TMP_423 TMP_424 TMP_426
+TMP_439) in (let TMP_441 \def (le_plus_plus TMP_416 TMP_417 TMP_419 TMP_421
+TMP_422 TMP_440) in (le_n_S TMP_411 TMP_415
+TMP_441))))))))))))))))))))))))))))))))))))))))) in (B_ind TMP_314 TMP_372
+TMP_407 TMP_442 b)))))) in (let TMP_457 \def (\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))).(let
+TMP_444 \def (weight_map f0 u2) in (let TMP_445 \def (weight_map f0 t2) in
+(let TMP_446 \def (plus TMP_444 TMP_445) in (let TMP_447 \def (weight_map g
+u1) in (let TMP_448 \def (weight_map g t1) in (let TMP_449 \def (plus TMP_447
+TMP_448) in (let TMP_450 \def (weight_map f0 u2) in (let TMP_451 \def
+(weight_map g u1) in (let TMP_452 \def (weight_map f0 t2) in (let TMP_453
+\def (weight_map g t1) in (let TMP_454 \def (H1 f0 g H4 H5) in (let TMP_455
+\def (H3 f0 g H4 H5) in (let TMP_456 \def (le_plus_plus TMP_450 TMP_451
+TMP_452 TMP_453 TMP_454 TMP_455) in (le_n_S TMP_446 TMP_449
+TMP_456))))))))))))))))))))))) in (K_ind TMP_307 TMP_443 TMP_457 k)))))))))))
+in (subst0_ind TMP_3 TMP_33 TMP_146 TMP_302 TMP_458 d u t z H)))))))))).