-lemma cpxs_inv_abbr1_dx (h) (p) (G) (L):
- ∀V1,T1,U2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 →
- ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
- U2 = ⓓ{p}V2.T2
- | ∃∃T2. ⦃G,L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = Ⓣ.
-#h #p #G #L #V1 #T1 #U2 #H
+lemma cpxs_inv_abbr1_dx (p) (G) (L):
+ ∀V1,T1,U2. ❨G,L❩ ⊢ ⓓ[p]V1.T1 ⬈* U2 →
+ ∨∨ ∃∃V2,T2. ❨G,L❩ ⊢ V1 ⬈* V2 & ❨G,L.ⓓV1❩ ⊢ T1 ⬈* T2 & U2 = ⓓ[p]V2.T2
+ | ∃∃T2. ❨G,L.ⓓV1❩ ⊢ T1 ⬈* T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ.
+#p #G #L #V1 #T1 #U2 #H