-lemma cpms_inv_abbr_sn_dx (n) (h) (G) (L):
- ∀p,V1,T1,X2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n,h] X2 →
- ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ➡*[h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓓ{p}V2.T2
- | ∃∃T2. ⦃G,L.ⓓV1⦄ ⊢ T1 ➡*[n ,h] T2 & ⬆*[1] X2 ≘ T2 & p = Ⓣ.
-#n #h #G #L #p #V1 #T1 #X2 #H
+lemma cpms_inv_abbr_sn_dx (h) (n) (G) (L):
+ ∀p,V1,T1,X2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
+ ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
+ | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
+#h #n #G #L #p #V1 #T1 #X2 #H