-lemma scpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, d1, d2] ⓛ{a}W2.T2 →
- ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
- ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, d2] T.
-#h #g #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H
+lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 →
+ ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W &
+ ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T.
+#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H