X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fequality.ma;h=a5d2f0d1e461cd5c02e95aa5f2eb1ec04f96d5fd;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;hp=a561827f8a83e1db22e18af1d836c10d572f3509;hpb=cd4e16d545b0ca42c37e2f79f63e6c25c6ad4480;p=helm.git

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index a561827f8..a5d2f0d1e 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -22,6 +22,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.