-lemma nta_ldef_drops (a) (h) (G) (K) (L) (i):
- ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
- ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[a,h] U.
-#a #h #G #K #L #i #V #W #HVW #U #HWU #HLK
+lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
+ ∀V,W. ⦃G,K⦄ ⊢ V :[h,a] W →
+ ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[h,a] U.
+#h #a #G #K #L #i #V #W #HVW #U #HWU #HLK