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