-lemma cpx_inv_flat1: ∀h,o,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h, o] U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 &
- U2 = ⓕ{I} V2. T2
- | (⦃G, L⦄ ⊢ U1 ➡[h, o] U2 ∧ I = Cast)
- | (⦃G, L⦄ ⊢ V1 ➡[h, o] U2 ∧ I = Cast)
- | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h, o] T2 &
- U1 = ⓛ{a}W1.T1 &
- U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl
- | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V & ⬆[0,1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h, o] T2 &
- U1 = ⓓ{a}W1.T1 &
- U2 = ⓓ{a}W2.ⓐV2.T2 & I = Appl.
-/2 width=3 by cpx_inv_flat1_aux/ qed-.
-
-lemma cpx_inv_appl1: ∀h,o,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[h, o] U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 &
- U2 = ⓐ V2. T2
- | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h, o] T2 &
- U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2
- | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V & ⬆[0,1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h, o] T2 &
- U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2. ⓐV2. T2.
-#h #o #G #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
-[ /3 width=5 by or3_intro0, ex3_2_intro/
-|2,3: #_ #H destruct
-| /3 width=11 by or3_intro1, ex5_6_intro/
-| /3 width=13 by or3_intro2, ex6_7_intro/
-]
+lemma cpx_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[h] U2 →
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
+ U2 = ⓝV2.T2
+ | ⦃G, L⦄ ⊢ U1 ⬈[h] U2
+ | ⦃G, L⦄ ⊢ V1 ⬈[h] U2.
+#h #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_cast1 … H) -H *
+/4 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex_intro/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpx_inv_zero1_pair: ∀h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[h] T2 →
+ T2 = #0 ∨
+ ∃∃V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2.
+#h #I #G #L #V1 #T2 * #c #H elim (cpg_inv_zero1_pair … H) -H *
+/4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/