X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fnf2%2Fdec.ma;h=eaaf4346a79f3fe3c7bafbf63c777d3b1a10cf09;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=37cc2b1165c0d5e6fe1d3ddbcd5c383ec899d695;hpb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
index 37cc2b116..eaaf4346a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma
@@ -95,7 +95,7 @@ x))).(\lambda (P: Prop).(let H8 \def (eq_ind T t1 (\lambda (t0: T).(subst0
 (clen c0) t t0 (lift (S O) (clen c0) x))) H4 (lift (S O) (clen c0) x) H7) in 
 (subst0_gen_lift_false x t (lift (S O) (clen c0) x) (S O) (clen c0) (clen c0) 
 (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) (\lambda (n: nat).(lt 
-(clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_comm 
+(clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen c0) (S O)) (plus_sym 
 (clen c0) (S O))) H8 P)))) (pr2_delta (CTail (Bind Abbr) t c0) (CSort x0) t 
 (clen c0) H6 t1 t1 (pr0_refl t1) (lift (S O) (clen c0) x) H4))))) H5)))) 
 (\lambda (H4: (eq T t1 (lift (S O) (clen c0) x))).(let H5 \def (eq_ind T t1 
@@ -128,7 +128,7 @@ x1)).(let H14 \def (eq_ind T x0 (\lambda (t0: T).(subst0 (clen c0) t t0 t2))
 H11 (lift (S O) (clen c0) x1) H12) in (subst0_gen_lift_false x1 t t2 (S O) 
 (clen c0) (clen c0) (le_n (clen c0)) (eq_ind_r nat (plus (S O) (clen c0)) 
 (\lambda (n: nat).(lt (clen c0) n)) (le_n (plus (S O) (clen c0))) (plus (clen 
-c0) (S O)) (plus_comm (clen c0) (S O))) H14 (eq T (lift (S O) (clen c0) x) 
+c0) (S O)) (plus_sym (clen c0) (S O))) H14 (eq T (lift (S O) (clen c0) x) 
 t2)))))) (pr0_gen_lift x x0 (S O) (clen c0) H10)))))) H8)) H7)))))) t1 H4))) 
 H3))) H2))) (or_introl (\forall (t2: T).((pr2 (CTail (Bind Abst) t c0) t1 t2) 
 \to (eq T t1 t2))) (ex2 T (\lambda (t2: T).((eq T t1 t2) \to (\forall (P: