update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx_lfxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma
index 69eab45f9821366ac42c87237171f129ba4e3b05..78b1302df163ea9dd8b2e380385f7fae6c1fa61a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma
@@ -17,7 +17,7 @@ include "basic_2/relocation/lexs_length.ma".
 include "basic_2/relocation/drops_lexs.ma".
 include "basic_2/static/frees_drops.ma".
 include "basic_2/static/lsubf_frees.ma".
-include "basic_2/static/lfxs.ma".
+include "basic_2/static/lfxs_fsle.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 include "basic_2/rt_transition/cpx_ext.ma".
 
@@ -160,7 +160,7 @@ lemma cpx_frees_conf_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
 qed-.
 
 (* Basic_2A1: uses: cpx_frees_trans *)
-lemma cpx_fle_comp: ∀h,G. R_fle_compatible (cpx h G).
+lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G).
 #h #G #L #T1 #T2 #HT12
 elim (frees_total L T1) #f1 #Hf1
 elim (cpx_frees_conf_lexs … Hf1 L … HT12) -HT12
@@ -168,7 +168,7 @@ elim (cpx_frees_conf_lexs … Hf1 L … HT12) -HT12
 qed-.
 
 (* Basic_2A1: uses: lpx_frees_trans *)
-lemma lfpx_fle_comp: ∀h,G. lfxs_fle_compatible (cpx h G).
+lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G).
 #h #G #L1 #L2 #T * #f1 #Hf1 #HL12
 elim (cpx_frees_conf_lexs h … Hf1 … HL12 T) // #f2 #Hf2
 lapply (lexs_fwd_length … HL12)