Add some proof steps

[Negabinary]

Overview

This branch adds new kinds of steps to the stepper

In particular it adds steps for:

• Cases (e.g. case on whether a boolean is true/false)
• Axioms (e.g. x * 0 = 0)
• Rewrites (write your own axiom and check it with a SAT solver)

We are also porting over the coq export from #1193 for basic axiom steps.

TODOS:

• Skel-based selection
• Fix hidden steps
• substitute variables in axioms
• fix closure issues
• add context to proofs
• Coq export for axioms
• Make selection select subtrees
• add inductive hypotheses to cases
• add an error message if cases don't end at the same value
• Fix duplicated ids in substitution
• Add conditions to axioms
• Add back the styling for hidden steps
• Prevent variable escape at the end of forall (last_step in forall)
• Require filling out under-specified rewrites
• Make the exp substitution more principled
• Fix capture in substitution
• Fix capture in evaluation etc
• Put rewrites in a box

After this pr:

• Add a Theorem keyword and put the proofs in splices
• Make the patterns in case actually patterns and run exhaustivity, redundancy, ...
• Pattern unpacking