-lemma cnv_fwd_fsb (a) (h):
- â\88\80G,L,T. â¦\83G,Lâ¦\84 â\8a¢ T ![a,h] â\86\92 â\89¥[h] ð\9d\90\92â¦\83G,L,Tâ¦\84.
-#a #h #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
+lemma cnv_fwd_fsb (h) (a):
+ â\88\80G,L,T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\89¥ð\9d\90\92 â\9dªG,L,Tâ\9d«.
+#h #a #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/