X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frdsx_csx.ma;h=355ecb0047ee0ed834785d5d966e77b368d68bec;hp=390ebe3cedaa84c35fa1fee9d9bf76b053ace2aa;hb=222044da28742b24584549ba86b1805a87def070;hpb=5c186c72f508da0849058afeecc6877cd9ed6303

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma
index 390ebe3ce..355ecb004 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_csx.ma
@@ -31,7 +31,7 @@ lemma rdsx_pair_lpxs (h) (o) (G):
 @rdsx_intro #Y #HY #HnY
 elim (lpx_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
 elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ]
-[ /5 width=5 by rdsx_lfdeq_trans, lpxs_step_dx, lfdeq_pair/
+[ /5 width=5 by rdsx_rdeq_trans, lpxs_step_dx, rdeq_pair/
 | @(IHV0 … HnV02) -IHV0 -HnV02
   [ /2 width=3 by lpxs_cpx_trans/
   | /3 width=3 by rdsx_lpx_trans, rdsx_cpx_trans/