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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
index 1939101a3..37015eb4f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpmuwe_csx.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/tweq_tdeq.ma".
+include "static_2/syntax/tweq_teqx.ma".
 include "basic_2/rt_computation/csx_cpxs.ma".
 include "basic_2/rt_computation/cpms_cpxs.ma".
 include "basic_2/rt_computation/cnuw_cnuw.ma".
@@ -31,7 +31,7 @@ elim (cnuw_dec_ex h G L T1)
 | * #n1 #T0 #HT10 #HnT10
   elim (IHT1 … T0) -IHT1
   [ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_trans, cpmuwe_intro, ex1_2_intro/
-  | /3 width=1 by tdeq_tweq/
+  | /3 width=1 by teqx_tweq/
   | /2 width=2 by cpms_fwd_cpxs/
   ]
 ]