-lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- â\88\80T1,U1. â\87§[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\87§[d, e] T2 ≡ U2 →
- L ⊢ U1 ⬌* U2 → K ⊢ T1 ⬌* T2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
+lemma cpcs_inv_lift: ∀G,L,K,s,l,m. ⬇[s, l, m] L ≡ K →
+ â\88\80T1,U1. â¬\86[l, m] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â¬\86[l, m] T2 ≡ U2 →
+ ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
+#G #L #K #s #l #m #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12