-lemma lsuba_aaa_trans: â\88\80G,L2,V,A. â¦\83G,L2â¦\84 ⊢ V ⁝ A →
- â\88\80L1. G â\8a¢ L1 â«\83â\81\9d L2 â\86\92 â¦\83G,L1â¦\84 ⊢ V ⁝ A.
+lemma lsuba_aaa_trans: â\88\80G,L2,V,A. â\9dªG,L2â\9d« ⊢ V ⁝ A →
+ â\88\80L1. G â\8a¢ L1 â«\83â\81\9d L2 â\86\92 â\9dªG,L1â\9d« ⊢ V ⁝ A.