From b273fb8dacc8ce058ffa4677846085864ace6b36 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 24 Jul 2006 14:09:30 +0000 Subject: [PATCH] equality now requires 2 extra parameters --- helm/software/matita/library/logic/equality.ma | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 0675edc76..95cb97307 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -65,7 +65,10 @@ default "equality" cic:/matita/logic/equality/sym_eq.con cic:/matita/logic/equality/trans_eq.con cic:/matita/logic/equality/eq_ind.con - cic:/matita/logic/equality/eq_elim_r.con. + cic:/matita/logic/equality/eq_elim_r.con + cic:/matita/logic/equality/eq_f.con + cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *) + theorem eq_f: \forall A,B:Type.\forall f:A\to B. \forall x,y:A. x=y \to f x = f y. -- 2.39.2