+lemma ntas_step_sn (h) (a) (G) (L):
+ ∀T1,T. ⦃G,L⦄ ⊢ T1 :[h,a] T →
+ ∀n,T2. ⦃G,L⦄ ⊢ T :*[h,a,n] T2 → ⦃G,L⦄ ⊢ T1 :*[h,a,↑n] T2.
+#h #a #G #L #T1 #T #H #n #T2 * #X2 #HT2 #HT #H1TX2 #H2TX2
+elim (cnv_inv_cast … H) -H #X1 #_ #HT1 #H1TX1 #H2TX1
+elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_sn #X #HX1 #HX2
+/3 width=5 by ntas_intro, cprs_trans, cpms_trans/
+qed-.
+
+lemma ntas_step_dx (h) (a) (G) (L):
+ ∀n,T1,T. ⦃G,L⦄ ⊢ T1 :*[h,a,n] T →
+ ∀T2. ⦃G,L⦄ ⊢ T :[h,a] T2 → ⦃G,L⦄ ⊢ T1 :*[h,a,↑n] T2.
+#h #a #G #L #n #T1 #T * #X1 #HT #HT1 #H1TX1 #H2TX1 #T2 #H
+elim (cnv_inv_cast … H) -H #X2 #HT2 #_ #H1TX2 #H2TX2
+elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_dx #X #HX1 #HX2
+/3 width=5 by ntas_intro, cprs_trans, cpms_trans/
+qed-.
+
+lemma nta_appl_ntas_zero (h) (a) (G) (L): ad a 0 →
+ ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → ∀p,T,U0. ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 →
+ ∀U. ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U → ⦃G,L⦄ ⊢ ⓐV.T :[h,a] ⓐV.ⓛ{p}W.U.
+#h #a #G #L #Ha #V #W #HVW #p #T #U0 #HTU0 #U #HU0
+lapply (nta_fwd_cnv_dx … HVW) #HW
+lapply (nta_bind_cnv … HW … HU0 p) -HW -HU0 #HU0
+elim (ntas_step_dx … HTU0 … HU0) -HU0 #X #HU #_ #HUX #HTX
+/4 width=9 by cnv_appl_ntas_ge, ntas_refl, cnv_cast, cpms_appl_dx/
+qed.
+
+lemma nta_appl_ntas_pos (h) (a) (n) (G) (L): ad a (↑n) →
+ ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U →
+ ∀p,U0. ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 → ⦃G,L⦄ ⊢ ⓐV.T :[h,a] ⓐV.U.
+#h #a #n #G #L #Ha #V #W #HVW #T #U #HTU #p #U0 #HU0
+elim (cnv_inv_cast … HTU) #X #_ #_ #HUX #HTX
+/4 width=11 by ntas_step_sn, cnv_appl_ntas_ge, cnv_cast, cpms_appl_dx/
+qed-.
+