add support for undefined values
This commit introduces proofs with quantified variables, which is potentially
expensive to reason with. Need testing with different Z3 solvers