X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Flift%2Ftlt.ma;h=4e088a12270bd030cc74ed1d1e7b8b7bca045471;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=316ebe839332905fde327bb545fe18b9d07bf883;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
index 316ebe839..4e088a122 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/lift/fwd.ma".
 
-
-include "lift/fwd.ma".
-
-include "tlt/props.ma".
+include "LambdaDelta-1/tlt/props.ma".
 
 theorem lift_weight_map:
  \forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to 
@@ -271,17 +269,9 @@ 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)).(let H0 \def (match H in le return (\lambda (n: 
-nat).(\lambda (_: (le ? n)).((eq nat n O) \to (eq nat (wadd f w m) (f m))))) 
-with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) O)).(let H1 \def (eq_ind 
-nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) 
-with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind 
-(eq nat (wadd f w m) (f m)) H1))) | (le_S m0 H0) \Rightarrow (\lambda (H1: 
-(eq nat (S m0) O)).((let H2 \def (eq_ind nat (S m0) (\lambda (e: nat).(match 
-e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
-\Rightarrow True])) I O H1) in (False_ind ((le (S m) m0) \to (eq nat (wadd f 
-w m) (f m))) H2)) H0))]) in (H0 (refl_equal nat O))))) (plus_n_O (wadd f w 
-O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal nat (f 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 (f m)))))))).
 
 theorem lift_tlt_dx:
  \forall (k: K).(\forall (u: T).(\forall (t: T).(\forall (h: nat).(\forall