/3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/
qed.
-lemma cprs_zeta: â\88\80G,L,V,T1,T,T2. â\87§[0, 1] T2 ≡ T →
+lemma cprs_zeta: â\88\80G,L,V,T1,T,T2. â¬\86[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/
qed.
lemma cprs_theta_dx: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
- â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â\87§[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+ â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â¬\86[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
/4 width=9 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_theta/