Simplify tactics state structure

[isovector]

Refinery implements the tactics search by growing a search tree and collapsing back the results of each branch. But this is a complicated thing to think about, because there is data moving in three different directions. The Judgement moves from root to leaves, while the "extract" moves from leaves to root --- and the TacticState moves sideways between branches, just to make things hard.

This PR formalizes the extract to as a dedicated type Synthesized (it corresponds to a synthesized attribute in the lingo of attribute grammars). Having this new conceptual clarity made me realize that I used to be using the TacticState as a hacky way of passing information back up the search tree. So this PR chops out a lot of that complexity and is more principled about how it implements the same behavior.

Specifically, it does the following things:

• Separate the creation of a local hypothesis (newly created bindings) from the introduction of them in the judgment
• Pushes these new local hypotheses into the extract, so that we have provenance information when scoring generated solutions
• Pushes used variables into the extract as well
• Greatly simplifies the TacticState structure, and removes a lot of imperative statefulness around that

The TacticState still contains some should-be-extract data about recursion usage, but that can't be removed until there are some changes upstream to refinery.

[jneira]

Nice summary, thanks