-lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}W1.T1 ⬌*[h] ⓛ{p2}W2.T2 →
- ∧∧ ⦃G,L⦄ ⊢ W1 ⬌*[h] W2 & ⦃G,L.ⓛW1⦄ ⊢ T1 ⬌*[h] T2 & p1 = p2.
+lemma cpcs_inv_abst_bi_sn (h) (G) (L):
+ ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
+ ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.