Improved the structure of the part of the prover that strips monotonic contexts off of a proof obligation. From here, it should be easy to parameterize the prover with custom monotonicty information.
restructured the monotonicity rewriter so that the results end up in the POs generated during testing. It is also more easily extendible