include "basic_2/rt_transition/lfpx_fsle.ma".
include "basic_2/rt_transition/lpx.ma".
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
-(* Properties with uncounted parallel rt-transition for local environments **)
+(* Properties with unbound parallel rt-transition for local environments ****)
lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
/2 width=1 by lfxs_lex/ qed.
-(* Inversion lemmas with uncounted parallel rt-transition for local envs ****)
+(* Inversion lemmas with unbound parallel rt-transition for local envs ******)
lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2.