IL: A conservative apartness checker

[nomeata]

This module adds a check

val apart : exp -> exp -> bool

with the idea that apart lhs1 lhs2 = true means that two reduction rules with these lhs definitely can’t match both.

I extracted it from my (rejected) proposal for how to desugar the otherwise construct, but I believe this check will be useful still, as (as far as I understand) Andreas wants to uphold and check the invariant that

Rules before a rule using otherwise must either obviously not match, or have syntactically equal LHSs, and only boolean premises.

The apart predicate is the “obviously not match”.

As of today, all rules in the reduction semantics have either eq or apart LHS, I believe.