-fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ➡[c, h] U2 →
- ∀J,V1,U1. U = ⓕ{J}V1.U1 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ➡[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ➡[cT, h] T2 &
- U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT
- | ∃∃cT. ⦃G, L⦄ ⊢ U1 ➡[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘
- | ∃∃cV. ⦃G, L⦄ ⊢ V1 ➡[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙
- | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ➡[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[cT, h] T2 &
- J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘
- | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ➡[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[cT, h] T2 &
- J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘.
-#c #h #G #L #U #U2 * -c -G -L -U -U2
-[ #I #G #L #J #W #U1 #H destruct
-| #G #L #s #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #I #G #L #V #T #U #i #_ #_ #J #W #U1 #H destruct
-| #rv #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #rv #cT #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=8 by or5_intro0, ex4_4_intro/
-| #c #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=3 by or5_intro1, ex3_intro/
-| #c #G #L #V1 #V2 #T #HV12 #J #W #U1 #H destruct /3 width=3 by or5_intro2, ex3_intro/
-| #rv #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=15 by or5_intro3, ex7_9_intro/
-| #rv #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=17 by or5_intro4, ex8_10_intro/
+fact cpg_inv_appl1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
+ ∀V1,U1. U = ⓐV1.U1 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+ U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
+ | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+ U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
+ | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+ U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
+[ #I #G #L #W #U1 #H destruct
+| #G #L #s #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #I #G #L #T #U #i #_ #_ #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #W #U1 #H destruct /3 width=8 by or3_intro0, ex4_4_intro/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T #T2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T2 #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #T #_ #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #W #U1 #H destruct /3 width=15 by or3_intro1, ex6_9_intro/
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #W #U1 #H destruct /3 width=17 by or3_intro2, ex7_10_intro/