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