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}.