From b86d8020e759afa1adcb8fe3571eeac288edfd83 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 15 Sep 2005 09:38:00 +0000 Subject: [PATCH] added \neq notation --- helm/matita/library/logic/equality.ma | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index a561827f8..84f7df2e6 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -15,6 +15,7 @@ set "baseuri" "cic:/matita/logic/equality/". include "higher_order_defs/relations.ma". +include "logic/connectives.ma". inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x. @@ -22,6 +23,10 @@ inductive eq (A:Type) (x:A) : A \to Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "leibnitz's equality" 'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y). +(*CSC: the URI must disappear: there is a bug now *) +interpretation "leibnitz's non-equality" + 'neq x y = (cic:/matita/logic/connectives/Not.con + (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)). theorem reflexive_eq : \forall A:Type. reflexive A (eq A). simplify.intros.apply refl_eq. -- 2.39.2