interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
+(* single = is for the abstract equality of setoids, == is for concrete
+ equalities (that may be lifted to the setoid level when needed *)
+notation < "hvbox(a break mpadded width -50% (=)= b)" non associative with precedence 45 for @{ 'eq_low $a $b }.
+notation > "a == b" non associative with precedence 45 for @{ 'eq_low $a $b }.
notation > "hvbox(a break =_0 b)" non associative with precedence 45
for @{ eq_rel ? (eq0 ?) $a $b }.