Some tidying in sptreeTheory.

- prove complete characterisation of lookup k (insert k' v t)
- get quicker proofs of domain_insert
- show domain (fromList l) and lookup k (fromList l) results