X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcprs.ma;h=e4c5460d09769a3c0285211a191baf0845baf0da;hb=1555848a5546d0154964286d3400114481d78962;hp=45c8cfe7dddd88c5ab0f36be5360c9fa152ec825;hpb=548f2d3f410c05e2eb332f5c2d074f5e6c6985e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index 45c8cfe7d..e4c5460d0 100644
--- 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.