lemma jsx_csx_conf (G):
∀L1,L2. G ⊢ L1 ⊒ L2 →
- â\88\80T. â\9dªG,L1â\9d« â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9dªG,L2â\9d« ⊢ ⬈*𝐒 T.
+ â\88\80T. â\9d¨G,L1â\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9d¨G,L2â\9d© ⊢ ⬈*𝐒 T.
/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
(* Properties with strongly rt-normalizing referred local environments ******)