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 REFERRED LOCAL ENVIRONMENTS ***********)
-(* Properties with uncounted parallel rt-transition for local environments **)
+(* Properties with syntactic equivalence for referred local environments ****)
-lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
+lemma fleq_lfpx (h) (G): ∀L1,L2,T. L1 ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
+/2 width=1 by lfeq_fwd_lfxs/ qed.
+
+(* Properties with unbound parallel rt-transition for full local envs *******)
+
+lemma lpx_lfpx: ∀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 full 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.