update for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_simple_teqo.ma

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 c56f1f718e3d75261543a0fce3bfad488b1d9042..70ee928ffdf951c5c0507c856da9989ab0afc452 100644 (file)
--- 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