From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Sep 2009 11:12:10 +0000 (+0000)
Subject: fixed eliminator name
X-Git-Tag: make_still_working~3506
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fcbc3084b02c8f69555fc97c59dca4a4b146eee8;p=helm.git

fixed eliminator name
---

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 70b12fcc5..093c85e13 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -503,7 +503,7 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply refl_eq.
 nqed.
 
-nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_ind_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
  nrewrite < (symmetric_eq … H1);
  napply H.