X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Fsubst1.ma;h=dc7c1df85c6f699cdda23cd4a561241b9fae5f42;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=6dfdb48e41d6fb58e96930a1faae4ee0ef882a98;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma
index 6dfdb48e4..dc7c1df85 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma
@@ -234,10 +234,10 @@ nat).(ty3 g a (TLRef (minus n (S O))) (lift n0 O t))) (ty3_abbr g (minus n (S
 O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abbr) u) a0 (csubst1_getl_ge d0 
 n (le_S_n d0 n (le_S (S d0) n H6)) c0 a0 u0 H4 (CHead d (Bind Abbr) u) H0) a 
 (S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le n0 n)) H6 
-(plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O 
-d0 n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_comm (S O) (minus 
-n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n 
-(S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0) 
+(plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O d0 
+n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_sym (S O) (minus n (S 
+O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n (S 
+O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0) 
 H6))))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: 
 C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst) 
 u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (e: 
@@ -371,10 +371,10 @@ nat).(ty3 g a (TLRef (minus n (S O))) (lift n0 O u))) (ty3_abst g (minus n (S
 O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abst) u) a0 (csubst1_getl_ge d0 
 n (le_S_n d0 n (le_S (S d0) n H6)) c0 a0 u0 H4 (CHead d (Bind Abst) u) H0) a 
 (S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le n0 n)) H6 
-(plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O 
-d0 n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_comm (S O) (minus 
-n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n 
-(S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0) 
+(plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n (le_lt_trans O d0 
+n (le_O_n d0) H6)))) (plus (S O) (minus n (S O))) (plus_sym (S O) (minus n (S 
+O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus O (minus n (S 
+O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0) 
 H6))))))))))))))))))))) (\lambda (c0: C).(\lambda (u: T).(\lambda (t: 
 T).(\lambda (_: (ty3 g c0 u t)).(\lambda (H1: ((\forall (e: C).(\forall (u0: 
 T).(\forall (d: nat).((getl d c0 (CHead e (Bind Abbr) u0)) \to (\forall (a0: 
@@ -739,12 +739,12 @@ n) (le_S (S d0) (plus O n) H5)) (le_O_n d0))) (eq_ind_r nat (S (minus n (S
 O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n (S O))) (lift n0 O t))) 
 (ty3_abbr g (minus n (S O)) a d u (getl_drop_conf_ge n (CHead d (Bind Abbr) 
 u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0) (\lambda (n0: nat).(le 
-n0 n)) H5 (plus d0 (S O)) (plus_comm d0 (S O)))) t H1) n (minus_x_SO n 
-(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O))) 
-(plus_comm (S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal 
-nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n 
-(le_O_n d0) H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda 
-(d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst) 
+n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1) n (minus_x_SO n 
+(le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n (S O))) (plus_sym 
+(S O) (minus n (S O)))) (S (plus O (minus n (S O)))) (refl_equal nat (S (plus 
+O (minus n (S O)))))) n (lt_plus_minus O n (le_lt_trans O d0 n (le_O_n d0) 
+H5))))))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: 
+C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abst) 
 u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (e: 
 C).(\forall (u0: T).(\forall (d0: nat).((getl d0 d (CHead e (Bind Void) u0)) 
 \to (\forall (a: C).((drop (S O) d0 d a) \to (ex3_2 T T (\lambda (y1: 
@@ -856,9 +856,9 @@ O))) (lift n O u) (eq_ind_r T (TLRef (plus (minus n (S O)) (S O))) (\lambda
 (eq_ind_r nat (S (minus n (S O))) (\lambda (n0: nat).(ty3 g a (TLRef (minus n 
 (S O))) (lift n0 O u))) (ty3_abst g (minus n (S O)) a d u (getl_drop_conf_ge 
 n (CHead d (Bind Abst) u) c0 H0 a (S O) d0 H4 (eq_ind_r nat (plus (S O) d0) 
-(\lambda (n0: nat).(le n0 n)) H5 (plus d0 (S O)) (plus_comm d0 (S O)))) t H1) 
+(\lambda (n0: nat).(le n0 n)) H5 (plus d0 (S O)) (plus_sym d0 (S O)))) t H1) 
 n (minus_x_SO n (le_lt_trans O d0 n (le_O_n d0) H5)))) (plus (S O) (minus n 
-(S O))) (plus_comm (S O) (minus n (S O)))) (S (plus O (minus n (S O)))) 
+(S O))) (plus_sym (S O) (minus n (S O)))) (S (plus O (minus n (S O)))) 
 (refl_equal nat (S (plus O (minus n (S O)))))) n (lt_plus_minus O n 
 (le_lt_trans O d0 n (le_O_n d0) H5))))))))))))))))))) (\lambda (c0: 
 C).(\lambda (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda