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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
index 936e655f1..35c106e6e 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
@@ -243,7 +243,7 @@ T).(pr2 a x1 x2))) (\lambda (x2: T).(\lambda (H25: (subst1 i u t
 x2)).(\lambda (H26: (subst1 i u (lift (S O) i x0) x2)).(let H27 \def (eq_ind 
 T x2 (\lambda (t0: T).(subst1 i u t t0)) H25 (lift (S O) i x0) 
 (subst1_gen_lift_eq x0 u x2 (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) 
-(\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_comm i 
+(\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) (plus_sym i 
 (S O))) H26)) in (ex_intro2 T (\lambda (x3: T).(subst1 i u t (lift (S O) i 
 x3))) (\lambda (x3: T).(pr2 a x1 x3)) x0 H27 (pr2_free a x1 x0 H10)))))) 
 (subst1_confluence_eq t4 t u i (subst1_single i u t4 t H2) (lift (S O) i x0) 
@@ -262,9 +262,9 @@ x3)).(let H17 \def (eq_ind T x2 (\lambda (t0: T).(subst1 d0 u0 t t0)) H13
 (minus i (S O)) (getl_drop_conf_ge i (CHead d (Bind Abbr) u) a0 
 (csubst1_getl_ge d0 i (le_S_n d0 i (le_S (S d0) i H12)) c0 a0 u0 H4 (CHead d 
 (Bind Abbr) u) H0) a (S O) d0 H5 (eq_ind_r nat (plus (S O) d0) (\lambda (n: 
-nat).(le n i)) H12 (plus d0 (S O)) (plus_comm d0 (S O)))) x1 x0 H10 x3 
+nat).(le n i)) H12 (plus d0 (S O)) (plus_sym d0 (S O)))) x1 x0 H10 x3 
 H16)))))) (subst1_gen_lift_ge u x0 x2 i (S O) d0 H14 (eq_ind_r nat (plus (S 
-O) d0) (\lambda (n: nat).(le n i)) H12 (plus d0 (S O)) (plus_comm d0 (S 
+O) d0) (\lambda (n: nat).(le n i)) H12 (plus d0 (S O)) (plus_sym d0 (S 
 O)))))))) (subst1_confluence_neq t4 t u i (subst1_single i u t4 t H2) (lift 
 (S O) d0 x0) u0 d0 H11 (sym_not_eq nat d0 i (lt_neq d0 i H12)))))))))) 
 (pr0_gen_lift x1 x (S O) d0 H7))))) (pr0_subst1 t3 t4 H1 u0 (lift (S O) d0