Prover to eliminate quantifiers in a PA formula. The prover is losely based on the idea in the paper "A Quantifier Elimination Algorithm for Linear Real Arithmetic" by David Monniaux, although it does not explicitly compute solutions of the matrix of a quantified formula like in the paper. Instead, the constraint extracted from an exhaustive subtree is injected as a lemma into other subtrees and used to close such subtrees earlier.

It is assumed that it is never necessary to adjust the constant freedom of a proof tree in this setting, because all constants that shield formulas also have to be eliminated constants and, thus, never occur in constraints anyway. This makes it possible to construct proof trees in a purely depth-first way (just like in the ModelSearchProver)

TODO: at the moment, this prover does not support theories like bit-vectors or multiplication