-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.