X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flpx_fsle.ma;h=f40b6b6276a95a0e196a4a39f82ad1b052657dff;hb=222044da28742b24584549ba86b1805a87def070;hp=7773a081ebd944614f6c7cdeaaa83c6cf8edfea7;hpb=05b047be6817f430c8c72fd9b0902df8bb9f579e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
index 7773a081e..f40b6b627 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_transition/lfpx_lpx.ma".
+include "basic_2/rt_transition/rpx_lpx.ma".
 
 (* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
 
@@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpx_lpx.ma".
 (* Basic_2A1: uses: lpx_cpx_frees_trans *)
 lemma lpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
                                  ∀L2. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
-/3 width=4 by lfpx_cpx_conf_fsge, lpx_lfpx/ qed-.
+/3 width=4 by rpx_cpx_conf_fsge, lpx_rpx/ qed-.
 
 (* Basic_2A1: uses: lpx_frees_trans *)
 lemma lpx_fsge_comp (h) (G): ∀L0,L2,T0. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄.