X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fscpds_scpds.ma;h=79923e2caea46df1ed75996537b70586d4aeded4;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=6c5de0687db8f4adccd043b4e73095e1783b858a;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
index 6c5de0687..79923e2ca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
@@ -43,7 +43,7 @@ lemma lstas_scpds_trans: ∀h,o,G,L,T1,T,T2,d1,d2,d.
 #h #o #G #L #T1 #T #T2 #d1 #d2 #d #Hd21 #HTd1 #HT1 * #T0 #d0 #Hd0 #HTd0 #HT0 #HT02
 lapply (lstas_da_conf … HT1 … HTd1) #HTd12
 lapply (da_mono … HTd12 … HTd0) -HTd12 -HTd0 #H destruct
-lapply (le_minus_to_plus_r … Hd21 Hd0) -Hd21 -Hd0
+lapply (le_minus_to_plus_c … Hd21 Hd0) -Hd21 -Hd0
 /3 width=7 by lstas_trans, ex4_2_intro/
 qed-.