for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
*)
notation > "hvbox(a break =_0 b)" non associative with precedence 45
-for @{ eq_rel ? (eq ?) $a $b }.
+for @{ eq_rel ? (eq0 ?) $a $b }.
notation > "hvbox(a break =_1 b)" non associative with precedence 45
for @{ eq_rel1 ? (eq1 ?) $a $b }.
notation > "hvbox(a break =_2 b)" non associative with precedence 45