-include "basic_2/static/lfxs_lfxs.ma".
-include "basic_2/rt_transition/lfpx_frees.ma".
-include "basic_2/rt_computation/lfpxs_fqup.ma".
-
-axiom cpx_frees_conf_lfpxs: ∀h,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
- ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T1] L2 →
- ∀g1. L2 ⊢ 𝐅*⦃T1⦄ ≡ g1 →
- ∃∃g2. L2 ⊢ 𝐅*⦃T2⦄ ≡ g2 & g2 ⊆ g1 & g1 ⊆ f1.
+include "basic_2/static/lfxs_lex.ma".
+include "basic_2/rt_transition/cpx_etc.ma".
+include "basic_2/rt_computation/lfpxs_lpxs.ma".