-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
+lemma cpms_inv_appl_sn (h) (n) (G) (L):
+ ∀V1,T1,X2. ❪G,L❫ ⊢ ⓐV1.T1 ➡*[h,n] X2 →
+ ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓐV2.T2
+ | ∃∃n1,n2,p,W,T. ❪G,L❫ ⊢ T1 ➡*[h,n1] ⓛ[p]W.T & ❪G,L❫ ⊢ ⓓ[p]ⓝW.V1.T ➡*[h,n2] X2 & n1 + n2 = n
+ | ∃∃n1,n2,p,V0,V2,V,T. ❪G,L❫ ⊢ V1 ➡*[h,0] V0 & ⇧[1] V0 ≘ V2 & ❪G,L❫ ⊢ T1 ➡*[h,n1] ⓓ[p]V.T & ❪G,L❫ ⊢ ⓓ[p]V.ⓐV2.T ➡*[h,n2] X2 & n1 + n2 = n.
+#h #n #G #L #V1 #T1 #U2 #H