Remove the need for `StateT` in the `SymEval` monad

[VictorCMiraldo]

Related to #137; we only have s StateT in our SymEval monad because of two reasons:

1. To generate unique names, but this is much more elegantly achieved through an approach such as "On Generating Unique Names", which is already implemented in the value-supply library; there's even this excellent writeup on SO: https://stackoverflow.com/questions/6311512/creating-unique-labels-in-haskell/63406066#63406066
2. To communicate constraints through the assume, prove and body terms in the prover. But this could be more easily handled by symbolically evaluating something like if assume (f i) i then (if prove i then () else bottom) else (), and make symbolic evaluation look for bottoms instead.

[VictorCMiraldo]

About issue number (2) above, one of the reasons that we do things in the current way is to be able to make progress (not only evaluate, but also prune!) things in "parallel". That is, if c then t else e will wait until it fully evaluates c to either True or False before looking at either t and e.

It is unclear to me whether this is an actual issue since the real work happens in the evaluation of f i and most of the pruning will happen in assume (f i) i anyway.

[VictorCMiraldo]

One interesting option here might be to define a "language transformer"

data SE lang

instance LanguageBuiltins lang => LanguageBuiltins (SE lang) where
  type BuiltinTerms = Either SymEvalTriple (BuiltinTerms lang)
   ...

Now we can inject any builtins we might need to treat in a special way directly into the symbolic engine. For example, SymEvalTriple build be a builtin that takes three terms: assume, prove and body. It can then be handled in a special way by the engine.

[VictorCMiraldo]

My attempt at (1) above is here: https://gist.github.com/VictorCMiraldo/0a0847759c1702efa96270b2b397e650