X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_cpxs.ma;h=8d066e53b8b3b302d63805fa4cba396d5864ee72;hb=58ea181757dce19b875b2f5a224fe193b2263004;hp=ae3d9a8892e37ac4d46ce87b0732aaf7c25f9c32;hpb=670ad7822d59e598a38d9037d482d3de188b170c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
index ae3d9a889..8d066e53b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
@@ -46,7 +46,7 @@ lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term.
 @IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2
 lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H
 elim (tdeq_cpxs_trans … HT02 … HTV2) -T2 #V0 #HTV0 #HV02
-lapply (tndeq_tdeq_canc_dx … H … HV02) -H #HnTV0
+lapply (tdneq_tdeq_canc_dx … H … HV02) -H #HnTV0
 elim (tdeq_dec h o T1 T0) #H
 [ lapply (tdeq_tdneq_trans … H … HnTV0) -H -HnTV0 #Hn10
   lapply (cpxs_trans … HT10 … HTV0) -T0 #H10