(* Properties with syntactic equivalence for referred local environments ****)
-lemma fleq_rpx (h) (G): â\88\80L1,L2,T. L1 â\89¡[T] L2 â\86\92 â¦\83G,L1â¦\84 ⊢ ⬈[h,T] L2.
+lemma fleq_rpx (h) (G): â\88\80L1,L2,T. L1 â\89¡[T] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[h,T] L2.
/2 width=1 by req_fwd_rex/ qed.
(* Properties with unbound parallel rt-transition for full local envs *******)
-lemma lpx_rpx: â\88\80h,G,L1,L2,T. â¦\83G,L1â¦\84 â\8a¢ â¬\88[h] L2 â\86\92 â¦\83G,L1â¦\84 ⊢ ⬈[h,T] L2.
+lemma lpx_rpx: â\88\80h,G,L1,L2,T. â\9dªG,L1â\9d« â\8a¢ â¬\88[h] L2 â\86\92 â\9dªG,L1â\9d« ⊢ ⬈[h,T] L2.
/2 width=1 by rex_lex/ qed.
(* Inversion lemmas with unbound parallel rt-transition for full local envs *)
-lemma rpx_inv_lpx_req: â\88\80h,G,L1,L2,T. â¦\83G,L1â¦\84 ⊢ ⬈[h,T] L2 →
- â\88\83â\88\83L. â¦\83G,L1â¦\84 ⊢ ⬈[h] L & L ≡[T] L2.
+lemma rpx_inv_lpx_req: â\88\80h,G,L1,L2,T. â\9dªG,L1â\9d« ⊢ ⬈[h,T] L2 →
+ â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈[h] L & L ≡[T] L2.
/3 width=3 by rpx_fsge_comp, rex_inv_lex_req/ qed-.