-lemma cprs_zeta: ∀L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
- L.ⓓV ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
-#L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+ ⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
+#G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx … H) -T1
+/3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/