-lemma cpxs_fpbg_trans (h): â\88\80G1,L1,T1,T. â¦\83G1,L1â¦\84 ⊢ T1 ⬈*[h] T →
- â\88\80G2,L2,T2. â¦\83G1,L1,Tâ¦\84 >[h] â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 >[h] â¦\83G2,L2,T2â¦\84.
+lemma cpxs_fpbg_trans (h): â\88\80G1,L1,T1,T. â\9dªG1,L1â\9d« ⊢ T1 ⬈*[h] T →
+ â\88\80G2,L2,T2. â\9dªG1,L1,Tâ\9d« >[h] â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« >[h] â\9dªG2,L2,T2â\9d«.