lemma nta_inv_ldec_sn_cnv (h) (a) (G) (K) (V):
∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[h,a] X2 →
- â\88\83â\88\83U. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & â¬\86*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![h,a].
+ â\88\83â\88\83U. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & â\87§*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![h,a].
#h #a #G #Y #X #X2 #H
elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct