lemma nta_inv_ldef_sn (h) (a) (G) (K) (V):
∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 :[h,a] X2 →
- â\88\83â\88\83W,U. â¦\83G,Kâ¦\84 â\8a¢ V :[h,a] W & â¬\86*[1] W ≘ U & ⦃G,K.ⓓV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓓV⦄ ⊢ X2 ![h,a].
+ â\88\83â\88\83W,U. â¦\83G,Kâ¦\84 â\8a¢ V :[h,a] W & â\87§*[1] W ≘ 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
lemma nta_inv_lref_sn (h) (a) (G) (L):
∀X2,i. ⦃G,L⦄ ⊢ #↑i :[h,a] X2 →
- â\88\83â\88\83I,K,T2,U2. â¦\83G,Kâ¦\84 â\8a¢ #i :[h,a] T2 & â¬\86*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![h,a] & L = K.ⓘ{I}.
+ â\88\83â\88\83I,K,T2,U2. â¦\83G,Kâ¦\84 â\8a¢ #i :[h,a] T2 & â\87§*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![h,a] & L = K.ⓘ{I}.
#h #a #G #L #X2 #i #H
elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
elim (cnv_inv_lref … H1) -H1 #I #K #Hi #H destruct
lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L):
∀X2,i. ⦃G,L⦄ ⊢ #i :[h,a] X2 →
- â\88¨â\88¨ â\88\83â\88\83K,V,W,U. â¬\87*[i] L â\89\98 K.â\93\93V & â¦\83G,Kâ¦\84 â\8a¢ V :[h,a] W & â¬\86*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]
- | â\88\83â\88\83K,W,U. â¬\87*[i] L â\89\98 K. â\93\9bW & â¦\83G,Kâ¦\84 â\8a¢ W ![h,a] & â¬\86*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a].
+ â\88¨â\88¨ â\88\83â\88\83K,V,W,U. â\87©*[i] L â\89\98 K.â\93\93V & â¦\83G,Kâ¦\84 â\8a¢ V :[h,a] W & â\87§*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]
+ | â\88\83â\88\83K,W,U. â\87©*[i] L â\89\98 K. â\93\9bW & â¦\83G,Kâ¦\84 â\8a¢ W ![h,a] & â\87§*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a].
#h #a #G #L #X2 #i #H
elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
elim (cnv_inv_lref_drops … H1) -H1 #I #K #V #HLK #HV
(* Note: "⦃G, L⦄ ⊢ U2 ⬌*[h] X2" can be "⦃G, L⦄ ⊢ X2 ➡*[h] U2" *)
lemma nta_inv_lifts_sn (h) (a) (G):
∀L,T2,X2. ⦃G,L⦄ ⊢ T2 :[h,a] X2 →
- â\88\80b,f,K. â¬\87*[b,f] L â\89\98 K â\86\92 â\88\80T1. â¬\86*[f] T1 ≘ T2 →
- â\88\83â\88\83U1,U2. â¦\83G,Kâ¦\84 â\8a¢ T1 :[h,a] U1 & â¬\86*[f] U1 ≘ U2 & ⦃G,L⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a].
+ â\88\80b,f,K. â\87©*[b,f] L â\89\98 K â\86\92 â\88\80T1. â\87§*[f] T1 ≘ T2 →
+ â\88\83â\88\83U1,U2. â¦\83G,Kâ¦\84 â\8a¢ T1 :[h,a] U1 & â\87§*[f] U1 ≘ U2 & ⦃G,L⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a].
#h #a #G #L #T2 #X2 #H #b #f #K #HLK #T1 #HT12
elim (cnv_inv_cast … H) -H #U2 #HX2 #HT2 #HXU2 #HTU2
lapply (cnv_inv_lifts … HT2 … HLK … HT12) -HT2 #HT1