X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Flift%2Ffwd.ma;h=824deac30887756bc8077bff678a180a47ab0b97;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=db188a2509d408206ac6df4acc03f979c10f2533;hpb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
index db188a250..824deac30 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
@@ -334,28 +334,27 @@ nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u t) (lift h d
 x))).(let H_x \def (lift_gen_head (Bind b) u t x h d H) in (let H0 \def H_x 
 in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Bind b) y 
 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: 
-T).(\lambda (z: T).(eq T t (lift h (s (Bind b) d) z)))) (ex3_2 T T (\lambda 
-(y: T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda (y: 
-T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: 
-T).(eq T t (lift h (S d) z))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda 
-(H1: (eq T x (THead (Bind b) x0 x1))).(\lambda (H2: (eq T u (lift h d 
-x0))).(\lambda (H3: (eq T t (lift h (s (Bind b) d) x1))).(eq_ind_r T (THead 
-(Bind b) x0 x1) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: 
-T).(eq T t0 (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u 
-(lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h (S d) z)))))) 
-(eq_ind_r T (lift h (s (Bind b) d) x1) (\lambda (t0: T).(ex3_2 T T (\lambda 
-(y: T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)))) 
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: 
-T).(\lambda (z: T).(eq T t0 (lift h (S d) z)))))) (eq_ind_r T (lift h d x0) 
-(\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead 
+T).(\lambda (z: T).(eq T t (lift h (S d) z)))) (ex3_2 T T (\lambda (y: 
+T).(\lambda (z: T).(eq T x (THead (Bind b) y z)))) (\lambda (y: T).(\lambda 
+(_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift 
+h (S d) z))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T x (THead 
+(Bind b) x0 x1))).(\lambda (H2: (eq T u (lift h d x0))).(\lambda (H3: (eq T t 
+(lift h (S d) x1))).(eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t0: 
+T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Bind b) y 
+z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: 
+T).(\lambda (z: T).(eq T t (lift h (S d) z)))))) (eq_ind_r T (lift h (S d) 
+x1) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead 
 (Bind b) x0 x1) (THead (Bind b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T 
-t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Bind b) 
-d) x1) (lift h (S d) z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: 
-T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)))) (\lambda (y: 
-T).(\lambda (_: T).(eq T (lift h d x0) (lift h d y)))) (\lambda (_: 
-T).(\lambda (z: T).(eq T (lift h (s (Bind b) d) x1) (lift h (S d) z)))) x0 x1 
-(refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d x0)) 
-(refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
+u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t0 (lift h (S d) 
+z)))))) (eq_ind_r T (lift h d x0) (\lambda (t0: T).(ex3_2 T T (\lambda (y: 
+T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)))) 
+(\lambda (y: T).(\lambda (_: T).(eq T t0 (lift h d y)))) (\lambda (_: 
+T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d) z)))))) (ex3_2_intro 
+T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Bind b) x0 x1) (THead (Bind 
+b) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T (lift h d x0) (lift h d 
+y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (S d) x1) (lift h (S d) 
+z)))) x0 x1 (refl_equal T (THead (Bind b) x0 x1)) (refl_equal T (lift h d 
+x0)) (refl_equal T (lift h (S d) x1))) u H2) t H3) x H1)))))) H0))))))))).
 
 theorem lift_gen_flat:
  \forall (f: F).(\forall (u: T).(\forall (t: T).(\forall (x: T).(\forall (h: 
@@ -369,26 +368,25 @@ nat).(\lambda (d: nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d
 x))).(let H_x \def (lift_gen_head (Flat f) u t x h d H) in (let H0 \def H_x 
 in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x (THead (Flat f) y 
 z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: 
-T).(\lambda (z: T).(eq T t (lift h (s (Flat f) d) z)))) (ex3_2 T T (\lambda 
-(y: T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda (y: 
-T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: 
-T).(eq T t (lift h d z))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: 
-(eq T x (THead (Flat f) x0 x1))).(\lambda (H2: (eq T u (lift h d 
-x0))).(\lambda (H3: (eq T t (lift h (s (Flat f) d) x1))).(eq_ind_r T (THead 
-(Flat f) x0 x1) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: 
-T).(eq T t0 (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u 
-(lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z)))))) 
-(eq_ind_r T (lift h (s (Flat f) d) x1) (\lambda (t0: T).(ex3_2 T T (\lambda 
-(y: T).(\lambda (z: T).(eq T (THead (Flat f) x0 x1) (THead (Flat f) y z)))) 
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: 
-T).(\lambda (z: T).(eq T t0 (lift h d z)))))) (eq_ind_r T (lift h d x0) 
-(\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead 
-(Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T 
-t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h (s (Flat f) 
-d) x1) (lift h d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq 
+T).(\lambda (z: T).(eq T t (lift h d z)))) (ex3_2 T T (\lambda (y: 
+T).(\lambda (z: T).(eq T x (THead (Flat f) y z)))) (\lambda (y: T).(\lambda 
+(_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift 
+h d z))))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T x (THead 
+(Flat f) x0 x1))).(\lambda (H2: (eq T u (lift h d x0))).(\lambda (H3: (eq T t 
+(lift h d x1))).(eq_ind_r T (THead (Flat f) x0 x1) (\lambda (t0: T).(ex3_2 T 
+T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f) y z)))) (\lambda 
+(y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_: T).(\lambda (z: 
+T).(eq T t (lift h d z)))))) (eq_ind_r T (lift h d x1) (\lambda (t0: 
+T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (THead (Flat f) x0 x1) 
+(THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d 
+y)))) (\lambda (_: T).(\lambda (z: T).(eq T t0 (lift h d z)))))) (eq_ind_r T 
+(lift h d x0) (\lambda (t0: T).(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq 
 T (THead (Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: 
+T).(eq T t0 (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T (lift h d 
+x1) (lift h d z)))))) (ex3_2_intro T T (\lambda (y: T).(\lambda (z: T).(eq T 
+(THead (Flat f) x0 x1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: 
 T).(eq T (lift h d x0) (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T 
-(lift h (s (Flat f) d) x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat 
-f) x0 x1)) (refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t 
-H3) x H1)))))) H0))))))))).
+(lift h d x1) (lift h d z)))) x0 x1 (refl_equal T (THead (Flat f) x0 x1)) 
+(refl_equal T (lift h d x0)) (refl_equal T (lift h d x1))) u H2) t H3) x 
+H1)))))) H0))))))))).