Multifunctions

Proof-aware multievaluation

We can define a version of multievaluate which is "proof-aware", in that, each evaluation step, multievaluate can also search through known assumptions and proofs, and use them if applicable to replace the term being evaluated (or parts of the term being evaluated) with other terms known to be equal given the known proofs and selected assumptions.

Todo

There are some efficiency questions to reason through here - obviously searching for all possible simplifications each step is not going to be performant - we may need to pass hints somehow of when simplification should be attempted.