support for forall in the SMT bridge

The implementation of this was relatively straightforward, but threw up a last
minute surprise. Simplification happens first *within* the quantified expression
with access to the constraints on the quantified variable. So, even without
explicit support for forall expressions, the following expression:

  forall x: 1 .. 2 do x = 1 | x = 2 end

will get simplified to

  forall x: 1 .. 2 do true end

We still need explicit forall support to collapse this resulting expression into
`true` and enable further simplification.