Syntax for defining relations as partial functions?

[jaccokrijnen]

Can we define binary relations as a set of equations, instead of an ADT? Perhaps we can then derive both the inference rules and decision procedures at the same time.