(* Inversion lemmas with uncounted parallel rt-transition for local envs ****)
lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
- â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h] L & L â\89¡[T] L2.
+ â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h] L & L â\89\90[T] L2.
/3 width=3 by lfpx_fsge_comp, lfxs_inv_lex_lfeq/ qed-.