X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_simple_teqo.ma;h=70ee928ffdf951c5c0507c856da9989ab0afc452;hb=adb9ba187619cea977d1d22971eba27eb437cd6a;hp=c56f1f718e3d75261543a0fce3bfad488b1d9042;hpb=f677b4ef7fa20f1ab36c5ee59598865d5c1b719b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
index c56f1f718..70ee928ff 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_teqo.ma
@@ -34,7 +34,7 @@ lemma csx_appl_simple_teqo (h) (G) (L):
 @csx_intro #X #HL #H
 elim (cpx_inv_appl1_simple … HL) -HL //
 #V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (tdneq_inv_pair … H) -H
+elim (tneqx_inv_pair … H) -H
 [ #H elim H -H //
 | -IHT1 #HV0
   @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10