+(* Properties with native type assignment for terms *************************)
+
+lemma nta_ntas (h) (a) (G) (L):
+ ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ T :*[h,a,1] U.
+#h #a #G #L #T #U #H
+elim (cnv_inv_cast … H) -H /2 width=3 by ntas_intro/
+qed-.
+
+(* Inversion lemmas with native type assignment for terms *******************)
+
+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
+(*
+lapply (nta_ntas … H) -H #H
+elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
+[ elim (eq_or_gt n) #H destruct
+ [ <minus_n_O in HU; #HU -Hn
+ /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
+ | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
+ <minus_n_n in HU; #HU
+ @or_intror
+ @(ex6_5_intro … Ha … HUX HX) -Ha -X
+ [2,4: /2 width=2 by ntas_inv_nta/
+ |6: @ntas_refl
+*)
+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-.
+