-lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
-#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
-lapply (da_inv_bind … Hd1) -Hd1 #Hd1
-elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
-elim (cprs_inv_abbr1 … H2) -H2 *
-[ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=6 by ex4_2_intro, ex3_intro/
+lemma cpms_inv_appl_sn (n) (h) (G) (L):
+ ∀V1,T1,X2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[n, h] X2 →
+ ∨∨ ∃∃V2,T2.
+ ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 &
+ X2 = ⓐV2.T2
+ | ∃∃n1,n2,p,W,T.
+ ⦃G, L⦄ ⊢ T1 ➡*[n1, h] ⓛ{p}W.T & ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V1.T ➡*[n2, h] X2 &
+ n1 + n2 = n
+ | ∃∃n1,n2,p,V0,V2,V,T.
+ ⦃G, L⦄ ⊢ V1 ➡*[h] V0 & ⬆*[1] V0 ≘ V2 &
+ ⦃G, L⦄ ⊢ T1 ➡*[n1, h] ⓓ{p}V.T & ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ➡*[n2, h] X2 &
+ n1 + n2 = n.
+#n #h #G #L #V1 #T1 #U2 #H
+@(cpms_ind_dx … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
+#n1 #n2 #U #U2 #_ * *
+[ #V0 #T0 #HV10 #HT10 #H #HU2 destruct
+ elim (cpm_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cpms_step_dx, or3_intro0, ex3_2_intro/
+ | #p #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
+ lapply (cprs_step_dx … HV10 … HV02) -V0 #HV12
+ lapply (lsubr_cpm_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
+ /5 width=8 by cprs_flat_dx, cpms_bind, cpm_cpms, lsubr_beta, ex3_5_intro, or3_intro1/
+ | #p #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ /6 width=12 by cprs_step_dx, cpm_cpms, cpm_appl, cpm_bind, ex5_7_intro, or3_intro2/
+ ]
+| #m1 #m2 #p #W #T #HT1 #HTU #H #HU2 destruct
+ lapply (cpms_step_dx … HTU … HU2) -U #H
+ @or3_intro1 @(ex3_5_intro … HT1 H) // (**) (* auto fails *)
+| #m1 #m2 #p #V2 #W2 #V #T #HV12 #HVW2 #HT1 #HTU #H #HU2 destruct
+ lapply (cpms_step_dx … HTU … HU2) -U #H
+ @or3_intro2 @(ex5_7_intro … HV12 HVW2 HT1 H) // (**) (* auto fails *)