From 7008966fdd5b3811852f60b459572a347be932a0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Feb 2007 14:48:46 +0000 Subject: [PATCH] restored coercions between eq and eq --- matita/library/logic/equality.ma | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma index 1f68503df..510f0c5c6 100644 --- a/matita/library/logic/equality.ma +++ b/matita/library/logic/equality.ma @@ -70,19 +70,24 @@ theorem eq_f': \forall A,B:Type.\forall f:A\to B. intros.elim H.apply refl_eq. qed. -(* +(* *) coercion cic:/matita/logic/equality/sym_eq.con. coercion cic:/matita/logic/equality/eq_f.con. -*) +(* *) default "equality" cic:/matita/logic/equality/eq.ind - cic:/matita/logic/equality/symmetric_eq.con + cic:/matita/logic/equality/sym_eq.con cic:/matita/logic/equality/transitive_eq.con cic:/matita/logic/equality/eq_ind.con cic:/matita/logic/equality/eq_elim_r.con cic:/matita/logic/equality/eq_f.con +(* *) + cic:/matita/logic/equality/eq_OF_eq.con. +(* *) +(* cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *) + *) theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C. \forall x1,x2:A. \forall y1,y2:B. -- 2.39.2