X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst0%2Ffwd.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst0%2Ffwd.ma;h=4b387483e16e9e23b29af037f9440f983b9f2842;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=43d9e4df30114d54265c07779be8cdc173719514;hpb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma
index 43d9e4df3..4b387483e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma
@@ -320,7 +320,7 @@ t2))))))))))) (\lambda (n: nat).(\lambda (x: T).(\lambda (i: nat).(\lambda
 T).(eq T x (lift h (S (plus i d)) t2))) (\lambda (t2: T).(subst0 i u (TLRef 
 n) t2))) (\lambda (H0: (lt n (S (plus i d)))).(let H1 \def (eq_ind T (lift h 
 (S (plus i d)) (TLRef n)) (\lambda (t: T).(subst0 i (lift h d u) t x)) H 
-(TLRef n) (lift_lref_lt n h (S (plus i d)) H0)) in (and_ind (eq nat n i) (eq 
+(TLRef n) (lift_lref_lt n h (S (plus i d)) H0)) in (land_ind (eq nat n i) (eq 
 T x (lift (S n) O (lift h d u))) (ex2 T (\lambda (t2: T).(eq T x (lift h (S 
 (plus i d)) t2))) (\lambda (t2: T).(subst0 i u (TLRef n) t2))) (\lambda (H2: 
 (eq nat n i)).(\lambda (H3: (eq T x (lift (S n) O (lift h d u)))).(eq_ind_r T 
@@ -338,7 +338,7 @@ O (lift h d u)) (lift h (S (plus i d)) t2))) (\lambda (t2: T).(subst0 i u
 (subst0_gen_lref (lift h d u) x i n H1)))) (\lambda (H0: (le (S (plus i d)) 
 n)).(let H1 \def (eq_ind T (lift h (S (plus i d)) (TLRef n)) (\lambda (t: 
 T).(subst0 i (lift h d u) t x)) H (TLRef (plus n h)) (lift_lref_ge n h (S 
-(plus i d)) H0)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n 
+(plus i d)) H0)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n 
 h)) O (lift h d u))) (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d)) 
 t2))) (\lambda (t2: T).(subst0 i u (TLRef n) t2))) (\lambda (H2: (eq nat 
 (plus n h) i)).(\lambda (_: (eq T x (lift (S (plus n h)) O (lift h d 
@@ -499,13 +499,13 @@ T).(\lambda (x: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (i:
 nat).(\lambda (H: (le d i)).(\lambda (H0: (lt i (plus d h))).(\lambda (H1: 
 (subst0 i u (lift h d (TLRef n)) x)).(\lambda (P: Prop).(lt_le_e n d P 
 (\lambda (H2: (lt n d)).(let H3 \def (eq_ind T (lift h d (TLRef n)) (\lambda 
-(t0: T).(subst0 i u t0 x)) H1 (TLRef n) (lift_lref_lt n h d H2)) in (and_ind 
+(t0: T).(subst0 i u t0 x)) H1 (TLRef n) (lift_lref_lt n h d H2)) in (land_ind 
 (eq nat n i) (eq T x (lift (S n) O u)) P (\lambda (H4: (eq nat n i)).(\lambda 
 (_: (eq T x (lift (S n) O u))).(let H6 \def (eq_ind nat n (\lambda (n0: 
 nat).(lt n0 d)) H2 i H4) in (le_false d i P H H6)))) (subst0_gen_lref u x i n 
 H3)))) (\lambda (H2: (le d n)).(let H3 \def (eq_ind T (lift h d (TLRef n)) 
 (\lambda (t0: T).(subst0 i u t0 x)) H1 (TLRef (plus n h)) (lift_lref_ge n h d 
-H2)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n h)) O u)) P 
+H2)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n h)) O u)) P 
 (\lambda (H4: (eq nat (plus n h) i)).(\lambda (_: (eq T x (lift (S (plus n 
 h)) O u))).(let H6 \def (eq_ind_r nat i (\lambda (n0: nat).(lt n0 (plus d 
 h))) H0 (plus n h) H4) in (le_false d n P H2 (lt_le_S n d (simpl_lt_plus_r h 
@@ -573,15 +573,15 @@ nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (subst0 i u (lift h d
 (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef 
 n) t2))) (\lambda (H1: (lt n d)).(let H2 \def (eq_ind T (lift h d (TLRef n)) 
 (\lambda (t: T).(subst0 i u t x)) H (TLRef n) (lift_lref_lt n h d H1)) in 
-(and_ind (eq nat n i) (eq T x (lift (S n) O u)) (ex2 T (\lambda (t2: T).(eq T 
-x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef n) t2))) 
+(land_ind (eq nat n i) (eq T x (lift (S n) O u)) (ex2 T (\lambda (t2: T).(eq 
+T x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef n) t2))) 
 (\lambda (H3: (eq nat n i)).(\lambda (_: (eq T x (lift (S n) O u))).(let H5 
 \def (eq_ind nat n (\lambda (n0: nat).(lt n0 d)) H1 i H3) in (le_false (plus 
 d h) i (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: 
 T).(subst0 (minus i h) u (TLRef n) t2))) H0 (le_plus_trans (S i) d h H5))))) 
 (subst0_gen_lref u x i n H2)))) (\lambda (H1: (le d n)).(let H2 \def (eq_ind 
 T (lift h d (TLRef n)) (\lambda (t: T).(subst0 i u t x)) H (TLRef (plus n h)) 
-(lift_lref_ge n h d H1)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S 
+(lift_lref_ge n h d H1)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S 
 (plus n h)) O u)) (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda 
 (t2: T).(subst0 (minus i h) u (TLRef n) t2))) (\lambda (H3: (eq nat (plus n 
 h) i)).(\lambda (H4: (eq T x (lift (S (plus n h)) O u))).(eq_ind nat (plus n 
@@ -597,9 +597,9 @@ d t2))) (\lambda (t2: T).(subst0 n u (TLRef n) t2)) (lift (S n) O u)
 h)) O u) t)) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(eq T (lift (S n0) O 
 u) (lift (plus h (S n)) O u))) (eq_ind_r nat (plus h (S n)) (\lambda (n0: 
 nat).(eq T (lift n0 O u) (lift (plus h (S n)) O u))) (refl_equal T (lift 
-(plus h (S n)) O u)) (S (plus h n)) (plus_n_Sm h n)) (plus n h) (plus_comm n 
+(plus h (S n)) O u)) (S (plus h n)) (plus_n_Sm h n)) (plus n h) (plus_sym n 
 h)) (lift h d (lift (S n) O u)) (lift_free u (S n) h O d (le_trans_plus_r O d 
-(plus O (S n)) (plus_le_compat O O d (S n) (le_n O) (le_S d n H1))) (le_O_n 
+(plus O (S n)) (le_plus_plus O O d (S n) (le_n O) (le_S d n H1))) (le_O_n 
 d))) (subst0_lref u n)) (minus (plus n h) h) (minus_plus_r n h)) x H4) i 
 H3))) (subst0_gen_lref u x i (plus n h) H2)))))))))))) (\lambda (k: 
 K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (i: nat).(\forall