-lemma rpx_cpx_conf_fsge_dx (h) (G): â\88\80L0,T0,T1. â¦\83G,L0â¦\84 ⊢ T0 ⬈[h] T1 →
- â\88\80L2. â¦\83G,L0â¦\84 â\8a¢â¬\88[h,T0] L2 â\86\92 â¦\83L2,T1â¦\84 â\8a\86 â¦\83L0,T1â¦\84.
+lemma rpx_cpx_conf_fsge_dx (h) (G): â\88\80L0,T0,T1. â\9dªG,L0â\9d« ⊢ T0 ⬈[h] T1 →
+ â\88\80L2. â\9dªG,L0â\9d« â\8a¢â¬\88[h,T0] L2 â\86\92 â\9dªL2,T1â\9d« â\8a\86 â\9dªL0,T1â\9d«.