X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_lpx.ma;h=845fc6d276bbc890def968b825524563e1327cbd;hp=3d9b9081c711ae5e4fd04f94df5486239e93a830;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hpb=613d8642b1154dde0c026cbdcd96568910198251

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
index 3d9b9081c..845fc6d27 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_lpx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "static_2/static/rex_lex.ma".
-include "basic_2/rt_transition/cpx_req.ma".
+include "basic_2/rt_transition/rpx_reqg.ma".
 include "basic_2/rt_transition/lpx.ma".
 
 (* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
@@ -35,7 +35,7 @@ lemma lpx_rpx (G) (T):
 lemma rpx_inv_req_lpx (G) (T):
       ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
       ∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2.
-/4 width=13 by cpx_req_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
+/4 width=13 by cpx_reqg_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
 
 (* Forward lemmas with extended rt-transition for full local envs ***********)