X2 = ⓐV2. T2
| ∃∃p,W,T. ⦃G,L⦄ ⊢ T1 ➡*[h] ⓛ{p}W.T &
⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V1.T ➡*[h] X2
- | â\88\83â\88\83p,V0,V2,V,T. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V0 & â¬\86*[1] V0 ≘ V2 &
+ | â\88\83â\88\83p,V0,V2,V,T. â¦\83G,Lâ¦\84 â\8a¢ V1 â\9e¡*[h] V0 & â\87§*[1] V0 ≘ V2 &
⦃G,L⦄ ⊢ T1 ➡*[h] ⓓ{p}V.T &
⦃G,L⦄ ⊢ ⓓ{p}V.ⓐV2.T ➡*[h] X2.
#h #G #L #V1 #T1 #X2 #H elim (cpms_inv_appl_sn … H) -H *