-interpretation "setoid3 eq" 'eq x y = (eq_rel3 _ (eq3 _) x y).
-interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
-interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
-interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
-
-notation < "hvbox(a break = \sub 1 b)" non associative with precedence 45
-for @{ 'eq1 $a $b }.
-
-notation < "hvbox(a break = \sub 2 b)" non associative with precedence 45
-for @{ 'eq2 $a $b }.
-
-notation < "hvbox(a break = \sub 3 b)" non associative with precedence 45
-for @{ 'eq3 $a $b }.
+interpretation "setoid3 eq" 'eq t x y = (eq_rel3 _ (eq3 t) x y).
+interpretation "setoid2 eq" 'eq t x y = (eq_rel2 _ (eq2 t) x y).
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 _ (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel _ (eq t) x y).