X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst1%2Fprops.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsubst1%2Fprops.ma;h=cb13ac64451b5dff408db314070afd7bd6802767;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=5a4059bfcaf148daf2a99ea6d863bb4a2b71bb38;hpb=84b0d9386906e5bf13bf3d0e6ea736e05ac9e8b8;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
index 5a4059bfc..cb13ac644 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma
@@ -138,7 +138,7 @@ nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O
 (TLRef h) (TLRef n) (lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) 
 (TLRef (plus h (S n))) (lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) 
 (sym_eq nat (S (plus h n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) 
-(plus_comm n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
+(plus_sym n h)) (plus n (S h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) 
 (lift_lref_ge n (S h) n (le_n n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt 
 n (S h) (S n) (le_n (S n)))) i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T 
 (TLRef (plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i