Optimisations and fixes

Added in length conjecture.

In-lined set constants.

Added in support for tuple constants via additional conditions to the
surrounding quantifier.

Added in optimisation for an assertion on a forall or exists.

Added in optimisation for a tuple load on a constant or known tuple
constructor.