include "basic_2/rt_transition/lfpx_fsle.ma".
include "basic_2/rt_transition/lpx.ma".
-(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
+(* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********)
-(* Properties with unbound 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 unbound 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.