+lemma ntas_inv_nta (h) (a) (G) (L):
+ ∀T,U. ❪G,L❫ ⊢ T :*[h,a,1] U → ❪G,L❫ ⊢ T :[h,a] U.
+#h #a #G #L #T #U
+* /2 width=3 by cnv_cast/
+qed-.
+
+(* Note: this follows from ntas_inv_appl_sn *)
+lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
+ ∀X. ❪G,L❫ ⊢ ⓐV.T :[h,a] X →
+ ∨∨ ∃∃p,W,U,U0. ad a 0 & ❪G,L❫ ⊢ V :[h,a] W & ❪G,L❫ ⊢ T :*[h,a,0] ⓛ[p]W.U0 & ❪G,L.ⓛW❫ ⊢ U0 :[h,a] U & ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.U ⬌*[h] X & ❪G,L❫ ⊢ X ![h,a]
+ | ∃∃n,p,W,U,U0. ad a (↑n) & ❪G,L❫ ⊢ V :[h,a] W & ❪G,L❫ ⊢ T :[h,a] U & ❪G,L❫ ⊢ U :*[h,a,n] ⓛ[p]W.U0 & ❪G,L❫ ⊢ ⓐV.U ⬌*[h] X & ❪G,L❫ ⊢ X ![h,a].
+#h #a #G #L #V #T #X #H
+(* Note: insert here: alternate proof in ntas_nta.etc *)
+elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
+elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
+elim (eq_or_gt n) #Hn destruct
+[ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 1) [| // ] <minus_n_O #U #H #HU0
+ lapply (cpms_appl_dx … V V … H) [ // ] -H #H
+ elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
+ lapply (cpms_trans … HX0 … HX01) -X0 #HX1
+ lapply (cprs_div … HUX1 … HX1) -X1 #HUX
+ lapply (cnv_cpms_trans … HT … HTU0) #H
+ elim (cnv_inv_bind … H) -H #_ #HU0
+ /4 width=8 by cnv_cpms_ntas, cnv_cpms_nta, ex6_4_intro, or_introl/
+| >(plus_minus_m_m_commutative … Hn) in HTU0; #H
+ elim (cpms_inv_plus … H) -H #U #HTU #HU0
+ lapply (cpms_appl_dx … V V … HTU) [ // ] #H
+ elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
+ lapply (cpms_trans … HX0 … HX01) -X0 #HX1
+ lapply (cprs_div … HUX1 … HX1) -X1 #HUX
+ <(S_pred … Hn) in Ha; -Hn #Ha
+ /5 width=10 by cnv_cpms_ntas, cnv_cpms_nta, cnv_cpms_trans, ex6_5_intro, or_intror/
+]
+qed-.