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=3dbbd61477d1c6f5ff21157c10d3fab207a5b059;hpb=863c1f7bb313c3d9dff08d60c8c7ef7c511263c4;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 3dbbd6147..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
@@ -144,7 +144,7 @@ i) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def
 h)))) (land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n0))))) 
 (or_intror (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land 
 (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n))) (conj (le (plus d h) 
-(plus n h)) (eq T (TLRef n) (TLRef n)) (plus_le_compat d n h h H0 (le_n h)) 
+(plus n h)) (eq T (TLRef n) (TLRef n)) (le_plus_plus d n h h H0 (le_n h)) 
 (refl_equal T (TLRef n)))) (minus (plus n h) h) (minus_plus_r n h)) i 
 H2)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (d: 
 nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to 
@@ -171,16 +171,16 @@ theorem lift_gen_lref_lt:
 d)).(\lambda (t: T).(\lambda (H0: (eq T (TLRef n) (lift h d t))).(let H_x 
 \def (lift_gen_lref t d h n H0) in (let H1 \def H_x in (or_ind (land (lt n d) 
 (eq T t (TLRef n))) (land (le (plus d h) n) (eq T t (TLRef (minus n h)))) (eq 
-T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(and_ind (lt 
-n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n d)).(\lambda 
-(H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 
-(TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2: (land (le 
-(plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind (le (plus d h) n) (eq T 
-t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus d h) 
-n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n 
-h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq T (TLRef 
-(minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S n) d h 
-H))) t H4))) H2)) H1)))))))).
+T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(land_ind 
+(lt n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n 
+d)).(\lambda (H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: 
+T).(eq T t0 (TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2: 
+(land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(land_ind (le (plus d 
+h) n) (eq T t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus 
+d h) n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef 
+(minus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq 
+T (TLRef (minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S 
+n) d h H))) t H4))) H2)) H1)))))))).
 
 theorem lift_gen_lref_false:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n 
@@ -192,12 +192,12 @@ n)).(\lambda (H0: (lt n (plus d h))).(\lambda (t: T).(\lambda (H1: (eq T
 (TLRef n) (lift h d t))).(\lambda (P: Prop).(let H_x \def (lift_gen_lref t d 
 h n H1) in (let H2 \def H_x in (or_ind (land (lt n d) (eq T t (TLRef n))) 
 (land (le (plus d h) n) (eq T t (TLRef (minus n h)))) P (\lambda (H3: (land 
-(lt n d) (eq T t (TLRef n)))).(and_ind (lt n d) (eq T t (TLRef n)) P (\lambda 
-(H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H H4))) H3)) 
-(\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind 
-(le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda (H4: (le (plus d h) 
-n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false (plus d h) n P H4 
-H0))) H3)) H2)))))))))).
+(lt n d) (eq T t (TLRef n)))).(land_ind (lt n d) (eq T t (TLRef n)) P 
+(\lambda (H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H 
+H4))) H3)) (\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n 
+h))))).(land_ind (le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda 
+(H4: (le (plus d h) n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false 
+(plus d h) n P H4 H0))) H3)) H2)))))))))).
 
 theorem lift_gen_lref_ge:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall 
@@ -208,14 +208,14 @@ n)).(\lambda (t: T).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d
 t))).(let H_x \def (lift_gen_lref t d h (plus n h) H0) in (let H1 \def H_x in 
 (or_ind (land (lt (plus n h) d) (eq T t (TLRef (plus n h)))) (land (le (plus 
 d h) (plus n h)) (eq T t (TLRef (minus (plus n h) h)))) (eq T t (TLRef n)) 
-(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(and_ind 
+(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(land_ind 
 (lt (plus n h) d) (eq T t (TLRef (plus n h))) (eq T t (TLRef n)) (\lambda 
 (H3: (lt (plus n h) d)).(\lambda (H4: (eq T t (TLRef (plus n h)))).(eq_ind_r 
 T (TLRef (plus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false d n (eq 
 T (TLRef (plus n h)) (TLRef n)) H (lt_le_S n d (simpl_lt_plus_r h n d 
 (lt_le_trans (plus n h) d (plus d h) H3 (le_plus_l d h))))) t H4))) H2)) 
 (\lambda (H2: (land (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
-h) h))))).(and_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
+h) h))))).(land_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
 h) h))) (eq T t (TLRef n)) (\lambda (_: (le (plus d h) (plus n h))).(\lambda 
 (H4: (eq T t (TLRef (minus (plus n h) h)))).(eq_ind_r T (TLRef (minus (plus n 
 h) h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (minus 
@@ -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))))))))).