From fcbc3084b02c8f69555fc97c59dca4a4b146eee8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Sep 2009 11:12:10 +0000 Subject: [PATCH] fixed eliminator name --- helm/software/matita/contribs/ng_assembly/common/theory.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 2.39.2