X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Ftlt%2Fprops.ma;h=72b13d733f8628b6a33c31dac064244daa8f3a60;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=56f46e4eae286831af1e6769628ac8386de984b2;hpb=d0982534aee06a30f91a06d2f3e82834b132a3d3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma
index 56f46e4ea..72b13d733 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "tlt/defs.ma".
+include "LambdaDelta-1/tlt/defs.ma".
 
 theorem wadd_le:
  \forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
@@ -88,7 +88,7 @@ t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
 nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus 
 (weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus 
 (weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1)) 
-(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S 
+(le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S 
 (weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g 
 H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0))) 
 (\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0)) 
@@ -100,31 +100,30 @@ t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f:
 (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat 
 \to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le 
 (f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1)) 
-(plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat 
-(weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map 
-(wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: 
-nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: 
-((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: 
-nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g 
-t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat \to 
+(plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map 
+f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1) 
+(H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O 
+(le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to 
 nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n)))) 
-\to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat \to 
-nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le (f 
-n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1)) 
-(plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat 
-(weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map 
-(wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: 
-nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) b)) (\lambda (_: F).(\lambda 
-(t0: T).(\lambda (H: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to 
-nat))).(((\forall (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t0) 
-(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f0: ((nat 
-\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g 
-n)))) \to (le (weight_map f0 t1) (weight_map g t1))))))).(\lambda (f0: ((nat 
-\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le 
-(f0 n) (g n))))).(le_n_S (plus (weight_map f0 t0) (weight_map f0 t1)) (plus 
-(weight_map g t0) (weight_map g t1)) (plus_le_compat (weight_map f0 t0) 
-(weight_map g t0) (weight_map f0 t1) (weight_map g t1) (H f0 g H1) (H0 f0 g 
-H1))))))))))) k)) t).
+\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda 
+(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g 
+t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to 
+nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus 
+(weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0) 
+(weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0) 
+(weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f 
+O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) 
+b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to 
+nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n)))) 
+\to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda 
+(H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall 
+(n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g 
+t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to 
+nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus 
+(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g 
+t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1) 
+(weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
 
 theorem weight_eq:
  \forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to