-interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
-interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) 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).
interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
interpretation "setoid symmetry" 'invert r = (sym ____ r).
notation ".= r" with precedence 50 for @{'trans $r}.
interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
interpretation "setoid symmetry" 'invert r = (sym ____ r).
notation ".= r" with precedence 50 for @{'trans $r}.