X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frsx_csx.ma;h=ee5d0e6132693daa8952fa1a1e25b05a3fb2412c;hp=c56d1c6ccfbe4462b087a349a35ca98a191b8c8f;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
index c56d1c6cc..ee5d0e613 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_csx.ma
@@ -28,7 +28,7 @@ fact rsx_fwd_lref_pair_csx_aux (G):
 @csx_intro #V2 #HV12 #HnV12
 @(IH … I) -IH [1,4: // | -HnV12 | -G #H ]
 [ /2 width=1 by lpx_pair/
-| elim (reqx_inv_zero_pair_sn … H) -H #Y #X #_ #H1 #H2 destruct -I
+| elim (reqg_inv_zero_pair_sn … H) -H #Y #X #_ #H1 #H2 destruct -I
   /2 width=1 by/
 ]
 qed-.
@@ -86,7 +86,7 @@ lemma rsx_lref_pair_lpxs (G):
 @rsx_intro #Y #HY #HnY
 elim (lpx_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
 elim (teqx_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ]
-[ /5 width=5 by rsx_reqx_trans, lpxs_step_dx, reqx_pair/
+[ /5 width=5 by rsx_reqx_trans, lpxs_step_dx, reqg_pair, reqg_refl/
 | @(IHV0 … HnV02) -IHV0 -HnV02
   [ /2 width=3 by lpxs_cpx_trans/
   | /3 width=3 by rsx_lpx_trans, rsx_cpx_trans/