TmOracle: Replace negative term equalities by refutable PmAltCons

The `PmExprEq` business was a huge hack and was at the same time vastly
too powerful and not powerful enough to encode negative term equalities,
i.e. facts of the form "forall y. x ≁ Just y".

This patch introduces the concept of 'refutable shapes': What matters
for the pattern match checker is being able to encode knowledge of the
kind "x can no longer be the literal 5" or "x can no longer be Just y,
for any y". We encode this knowledge in a `PmRefutEnv`, mapping a set of
newly introduced `PmAltCon`s (literals and `ConLike`s) to eac variable
denoting above inequalities.

So, say we have `x ≁ Just ∈ refuts` in the term oracle context and
try to solve an equality like `x ~ Just 5`. The entry in the refutable
environment will immediately lead to a contradiction.

This machinery renders the whole `PmExprEq` business unnecessary,
getting rid of a lot of (mostly dead) code.

Note that the `PmAltConLike` case is currently unnecessary: The `ConVar`
case will just split the value set abstraction for each possible
constructor instead of encoding negative equalites. This is bound to
change in a follow-up patch. If we began to use `PmAltConLike`, we'd
even profit from nicer error messages as is currently the case for
negative literal equalities.

See the Note [Refutable shapes] in TmOracle for a place to start.