Parsing of SMT results back into types.
Add an instance of the external solver to the TcSMonad
Separate terms by a space.
Evidence for proofs generate by external solver
Fix strictness bug; add `extSolProve` to the interface.
Fix definition of `push`; add a TcS wrapper form `extSolProve`.
The external solver stage (incomplete, improvement is missing)