- | (⦃G, L⦄ ⊢ U1 ➡ U2 ∧ I = Cast)
- | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ W1 ➡ W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 &
- U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl
- | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V & ⬆[0,1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 &
- U1 = ⓓ{a}W1.T1 &
- U2 = ⓓ{a}W2.ⓐV2.T2 & I = Appl.
-/2 width=3 by cpr_inv_flat1_aux/ qed-.
-
-(* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
-lemma cpr_inv_appl1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡ U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 &
- U2 = ⓐV2.T2
- | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ W1 ➡ W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡ T2 &
- U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2
- | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V & ⬆[0,1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 &
- U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2.
-#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5 by or3_intro0, ex3_2_intro/
-| #_ #H destruct
-| /3 width=11 by or3_intro1, ex5_6_intro/
-| /3 width=13 by or3_intro2, ex6_7_intro/
-]
-qed-.
-
-(* Note: the main property of simple terms *)
-lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ T1 ➡ T2 &
- U = ⓐV2. T2.
-#G #L #V1 #T1 #U #H #HT1
-elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5 by ex3_2_intro/
-| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
- elim (simple_inv_bind … HT1)
-| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
- elim (simple_inv_bind … HT1)
-]
-qed-.
-
-(* Basic_1: includes: pr0_gen_cast pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡ U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 &
- U2 = ⓝ V2. T2
- ) ∨ ⦃G, L⦄ ⊢ U1 ➡ U2.
-#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5 by ex3_2_intro, or_introl/
-| /2 width=1 by or_intror/
-| #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct
-| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
+ | (⦃G,L⦄ ⊢ U1 ➡[h] U2 ∧ I = Cast)
+ | ∃∃p,V2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L⦄ ⊢ W1 ➡[h] W2 &
+ ⦃G,L.ⓛW1⦄ ⊢ T1 ➡[h] T2 & U1 = ⓛ{p}W1.T1 &
+ U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
+ | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V & ⇧*[1] V ≘ V2 &
+ ⦃G,L⦄ ⊢ W1 ➡[h] W2 & ⦃G,L.ⓓW1⦄ ⊢ T1 ➡[h] T2 &
+ U1 = ⓓ{p}W1.T1 &
+ U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
+#h * #G #L #V1 #U1 #U2 #H
+[ elim (cpm_inv_appl1 … H) -H *
+ /3 width=13 by or4_intro0, or4_intro2, or4_intro3, ex7_7_intro, ex6_6_intro, ex3_2_intro/
+| elim (cpr_inv_cast1 … H) -H [ * ]
+ /3 width=5 by or4_intro0, or4_intro1, ex3_2_intro, conj/