-lemma xpr_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\9e¸[g] U → L ⊢ U ⁝ A.
-#h #g #L #T #A #HT #U * [2: * ] /2 width=3/ /2 width=6/
+lemma xpr_aaa: â\88\80h,g,L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80U. â¦\83h, Lâ¦\84 â\8a¢ T â\80¢â\9e¡[g] U → L ⊢ U ⁝ A.
+#h #g #L #T #A #HT #U * /2 width=3/ /2 width=6/