Simplification - Improvement Proposals

One major component of the Haskell backend is the simplifier. It takes care of:

• function evaluation
• lemma application (simplification rules)
• ML reasoning, simplifying predicates to some normalized form
• sending predicates to the SMT solver

We'd like to know what users' experiences with the simplifier are and what changes they would like to see.

Any ideas are welcome, so feel free to "think big". For example, I would like to be able to step through the simplification procedure, like a "functional" kore-repl.

Start by surveying the Haskell backend's simplifier, including function evaluation, lemma application, ML predicate normalization, and SMT-solver interaction. Review the existing discussion and user experiences, then define a concrete, agreed improvement with clear completion criteria; the issue's example is a step-through experience similar to a functional kore-repl.