perf: use a custom `contradiction` when proving `match` equations (#16460)

This PR makes generating the equations of a `match` with many
alternatives faster when the patterns contain literals nested in
constructors, e.g., `| some "a" => ..`. For 32 alternatives of this
form, generating the `match` equations takes 0.53s instead of 1.45s.

The equation proofs used the general `contradiction` tactic, which looks
for a pair of hypotheses `h₁ : p` and `h₂ : ¬ p` by comparing every
hypothesis of the form `p → False` with every other hypothesis. The
goals of these proofs have one such hypothesis for each alternative, and
the tactic is tried on two goals per alternative, so the proof of the
catch-all equation was cubic in the number of alternatives. The proofs
now use `contradictionForEqns`, which only performs the checks that
close these goals: a disequality between definitionally equal terms, a
generalized disequality (`processGenDiseq`), and an element of an empty
type.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5.2 <noreply@anthropic.com>