-lemma nta_appl_abst (a) (h) (p) (G) (L):
- ∀n. appl a n →
- â\88\80V,W. â¦\83G,Lâ¦\84 â\8a¢ V :[a,h] W →
- â\88\80T,U. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T :[a,h] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T :[a,h] â\93\90V.â\93\9b{p}W.U.
-#a #h #p #G #L #n #Ha #V #W #H1 #T #U #H2
+lemma nta_appl_abst (h) (a) (p) (G) (L):
+ ∀n. ad a n →
+ â\88\80V,W. â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W →
+ â\88\80T,U. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T :[h,a] â\93\90V.â\93\9b[p]W.U.
+#h #a #p #G #L #n #Ha #V #W #H1 #T #U #H2