-lemma cpcs_inv_abst_sn (h) (G) (L): â\88\80p1,p2,W1,W2,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ â\93\9b{p1}W1.T1 â¬\8c*[h] â\93\9b{p2}W2.T2 →
- â\88§â\88§ â¦\83G, Lâ¦\84 â\8a¢ W1 â¬\8c*[h] W2 & â¦\83G, L.â\93\9bW1â¦\84 ⊢ T1 ⬌*[h] T2 & p1 = p2.
+lemma cpcs_inv_abst_sn (h) (G) (L): â\88\80p1,p2,W1,W2,T1,T2. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p1]W1.T1 â¬\8c*[h] â\93\9b[p2]W2.T2 →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ W1 â¬\8c*[h] W2 & â\9dªG,L.â\93\9bW1â\9d« ⊢ T1 ⬌*[h] T2 & p1 = p2.