fix: performance issue when elaborating match-expressions with many literals

This PR fixes a performance issue that occurs when generating equation
lemmas for functions that use match-expressions containing several
literals. This issue was exposed by #9322 and arises from a combination of factors:

1. Literal values are compiled into a chain of dependent if-then-else expressions.
2. Dependent if-then-else expressions are significantly more expensive to simplify than regular ones.
3. The `split` tactic selects a target, splits it, and then invokes `simp` on the resulting subgoals. Moreover, `simp` traverses the entire goal bottom-up and does not stop after reaching the target.

This PR addresses the issue by introducing a custom simproc that
avoids recursively simplifying nested if-then-else expressions. It
does **not** alter the user-facing behavior of the `split` tactic
because such a change would be highly disruptive. Instead, the PR adds
a new flag, `backward.split` to control the behavior of the
user-facing `split` tactic. It is currently set to `true`, i.e., the
old behavior is still the default one. In a future PR, we should set
this flag to `false` by default and begin repairing all affected
proofs.

closes #9322