-lemma cnv_appl_ge (a) (h) (n1) (p) (G) (L):
- ∀n2. n1 ≤ n2 → appl a n2 →
- â\88\80V. â¦\83G,Lâ¦\84 â\8a¢ V ![a,h] â\86\92 â\88\80T. â¦\83G,Lâ¦\84 â\8a¢ T ![a,h] →
- â\88\80X. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] X â\86\92 â\88\80W. â¦\83G,Lâ¦\84 ⊢ W ➡*[h] X →
- â\88\80U. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n1,h] â\93\9b{p}W.U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.T ![a,h].
-#a #h #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX
+lemma cnv_appl_ge (h) (a) (n1) (p) (G) (L):
+ ∀n2. n1 ≤ n2 → ad a n2 →
+ â\88\80V. â\9dªG,Lâ\9d« â\8a¢ V ![h,a] â\86\92 â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] →
+ â\88\80X. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] X â\86\92 â\88\80W. â\9dªG,Lâ\9d« ⊢ W ➡*[h] X →
+ â\88\80U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n1,h] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T ![h,a].
+#h #a #n1 #p #G #L #n2 #Hn12 #Ha #V #HV #T #HT #X #HVX #W #HW #X #HTX