Symbolic term evaluation

[joom]

Currently all term evaluation gets stuck, so we end up with terms like 1 + 1. It's not possible to prove things like P(1 + 1) |- P(2) without the Z3 rule, but it should be.