Model-parameterized equality

[kris-brown]

If we have two FinFunctions (f and g) they may be different f != g but may be equivalent in a model-specific, idiosyncratic way (e.g. have the same input-output behavior, which is sufficient for equality in FinSet).

For any theory and any type constructor this is a common problem. A general solution would be to allow adding a method to Base.:(==) in the @instance macro. This would allow one to still have f != g while having a uniform way to check (e.g. within a @withmodel block) whether or not they are equal from the model's perspective.