-lemma nta_bind_cnv (a) (h) (G) (K):
- ∀V. ⦃G,K⦄ ⊢ V ![a,h] →
- ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U →
- ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U.
-#a #h #G #K #V #HV #I #T #U #H #p
+lemma nta_bind_cnv (h) (a) (G) (K):
+ ∀V. ⦃G,K⦄ ⊢ V ![h,a] →
+ ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h,a] U →
+ ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[h,a] ⓑ{p,I}V.U.
+#h #a #G #K #V #HV #I #T #U #H #p