-lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 →
- T2 = #i ∨
- ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 &
- ⬆[0, i+1] T1 ≡ T2.
-#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
+lemma cpxs_inv_zero1 (G) (L):
+ ∀T2. ❪G,L❫ ⊢ #0 ⬈* T2 →
+ ∨∨ T2 = #0
+ | ∃∃I,K,V1,V2. ❪G,K❫ ⊢ V1 ⬈* V2 & ⇧[1] V2 ≘ T2 & L = K.ⓑ[I]V1.
+#G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
+#T #T2 #_ #HT2 *
+[ #H destruct
+ elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
+ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
+| * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
+ elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
+ /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
+]
+qed-.
+
+lemma cpxs_inv_lref1 (G) (L):
+ ∀T2,i. ❪G,L❫ ⊢ #↑i ⬈* T2 →
+ ∨∨ T2 = #(↑i)
+ | ∃∃I,K,T. ❪G,K❫ ⊢ #i ⬈* T & ⇧[1] T ≘ T2 & L = K.ⓘ[I].
+#G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/