- name changes in the rediction rules

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 45c8cfe7dddd88c5ab0f36be5360c9fa152ec825..e4c5460d09769a3c0285211a191baf0845baf0da 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -91,9 +91,9 @@ lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
 /3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
 qed.
 
-lemma cprs_tau: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
+lemma cprs_eps: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
 #G #L #T1 #T2 #H @(cprs_ind … H) -T2
-/3 width=3 by cprs_strap1, cpr_cprs, cpr_tau/
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_eps/
 qed.
 
 lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2.