-theorem cpc_conf: â\88\80h,G,L,T0,T1,T2. â¦\83G,Lâ¦\84 â\8a¢ T0 â¬\8c[h] T1 â\86\92 â¦\83G,Lâ¦\84 ⊢ T0 ⬌[h] T2 →
- â\88\83â\88\83T. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\8c[h] T & â¦\83G,Lâ¦\84 ⊢ T2 ⬌[h] T.
+theorem cpc_conf: â\88\80h,G,L,T0,T1,T2. â\9dªG,Lâ\9d« â\8a¢ T0 â¬\8c[h] T1 â\86\92 â\9dªG,Lâ\9d« ⊢ T0 ⬌[h] T2 →
+ â\88\83â\88\83T. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\8c[h] T & â\9dªG,Lâ\9d« ⊢ T2 ⬌[h] T.