Helpers for checking proof obligations

[langston-barrett]

We check proof obligations that come from Crucible a lot:

https://github.com/GaloisInc/crucible/blob/f9760bdb9921523848efc9889fbd72bd6dea506e/crucible-symio/tests/TestMain.hs#L151C3-L151C31

https://github.com/GaloisInc/macaw/blob/645754178a034c22e97aac49a962c99b387aaa01/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L330

https://github.com/GaloisInc/surveyor/blob/96b6748d811bc2ab9ef330307a324bd00e04819f/crux-dbg/src/Crux/Debug/LLVM/Overrides.hs#L161

https://github.com/GaloisInc/mss/blob/ca97f1bc6b296b30bcccad3b4098544d91427103/grackle/src/Grackle/Overrides/Utils.hs#L84

https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Verifier/Prove.hs#L137

As seen above, most of these instances use somewhat low-level What4 functions, and require thinking about the encoding of proof assumptions and obligations into a SMT-compatible format (in particular, they inline the material conditional). This PR introduces more high-level helpers. Doing so required a bit of refactoring.

[langston-barrett]

This PR moves in the direction of deduplicating code that proves goals. In the future, it would be nice to improve these helpers by:

• Allowing "fast failure" on conjunctions of goals (i.e., not attempting to prove the RHS if the LHS is disproved)
• Parallelization and timeouts of solver queries (see the ambient-verifier link above)
• Use of push/pop in an online solver, rather than distributing assumptions into goals

[RyanGlScott]

This looks like a nice cleanup. I only have minor suggestions.