- name changes in the rediction rules

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnr_crr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
index 35937fb419baac44a98bc2821415f97dbac8d4a1..e1d75cd047651492c877f59fb888ad817a776bc0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma
@@ -30,7 +30,7 @@ lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 
   elim (cnr_inv_appl … H) -H /2 width=1/
 | #I #L #V #T * #H1 #H2 destruct
   [ elim (cnr_inv_zeta … H2)
-  | elim (cnr_inv_tau … H2)
+  | elim (cnr_inv_eps … H2)
   ]
 |5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
   [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/