-lemma cpcs_inv_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\87§[d, e] T2 â\89¡ U2 →
+lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K →
+ â\88\80T1,U1. â¬\86[l, k] T1 â\89\98 U1 â\86\92 â\88\80T2,U2. â¬\86[l, k] T2 â\89\98 U2 →