Spurious interpretation removed.

[helm.git] / helm / matita / library / list / list.ma

diff --git a/helm/matita/library/list/list.ma b/helm/matita/library/list/list.ma
index 417c88ee78acbacfde334c794d3b60293a95199a..0b7340d051ce5fc1f34e4f5480bea986df6c5247 100644 (file)
--- a/helm/matita/library/list/list.ma
+++ b/helm/matita/library/list/list.ma
@@ -16,9 +16,6 @@ set "baseuri" "cic:/matita/list/".
 include "logic/equality.ma".
 include "higher_order_defs/functions.ma".
 
-interpretation "leibnitz's equality" 'eq x y =
-  (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
-
 notation "hvbox(hd break :: tl)"
   right associative with precedence 46
   for @{'cons $hd $tl}.