From 9d873748bec82cef7ff10ce660e6f89505871dbe Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Jul 2006 09:04:25 +0000 Subject: [PATCH] added definition of f_equal1. I think this file should not be inside the matita library! once cercions from /\ to eq will be committed the definition should be replaced by two coercion statement (that will generate the composite) --- helm/software/matita/library/legacy/coq.ma | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma index e7a5615d9..8669d1ef7 100644 --- a/helm/software/matita/library/legacy/coq.ma +++ b/helm/software/matita/library/legacy/coq.ma @@ -19,7 +19,9 @@ default "equality" cic:/Coq/Init/Logic/sym_eq.con cic:/Coq/Init/Logic/trans_eq.con cic:/Coq/Init/Logic/eq_ind.con - cic:/Coq/Init/Logic/eq_ind_r.con. + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/f_equal.con + cic:/Coq/Init/Logic/f_equal1.con. default "true" cic:/Coq/Init/Logic/True.ind. @@ -74,3 +76,9 @@ interpretation "Coq's natural 'not less or equal than'" 'nleq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)). +theorem f_equal1 : + \forall A,B:Type. \forall f:A \to B. \forall x,y:A. + x = y \to f y = f x. + intros.elim H.reflexivity. +qed. + -- 2.39.2