-lemma nta_conv (a) (h) (G) (L) (T):
- â\88\80U1. â¦\83G,Lâ¦\84 â\8a¢ T :[a,h] U1 →
- â\88\80U2. â¦\83G,Lâ¦\84 ⊢ U1 ⬌*[h] U2 →
- â\88\80W2. â¦\83G,Lâ¦\84 â\8a¢ U2 :[a,h] W2 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T :[a,h] U2.
-#a #h #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2
+lemma nta_conv (h) (a) (G) (L) (T):
+ â\88\80U1. â\9d¨G,Lâ\9d© â\8a¢ T :[h,a] U1 →
+ â\88\80U2. â\9d¨G,Lâ\9d© ⊢ U1 ⬌*[h] U2 →
+ â\88\80W2. â\9d¨G,Lâ\9d© â\8a¢ U2 :[h,a] W2 â\86\92 â\9d¨G,Lâ\9d© â\8a¢ T :[h,a] U2.
+#h #a #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2