licenses: convert license tags to SPDX

lib: restructure the instantiations type of Trace_Schematic_Insts

This allows us to explicitly record the bound variables from the subgoal so that
they can be more easily handled. We also now drop binders when constructing typ
instantiations.

lib: improve message printing for crunch and wp, and refactor common printing functions

lib: add utilities for using options.

lib: add an implementation of the sum type

lib: don't extend core signatures.

Just because we *can* extend the core SML `List` signature, that doesn't
mean we *should*. It's a neat trick, but it makes it harder to find uses
of the new modules, and obfuscates definitions for very little gain.

lib: add ML utilties 'bucket' file.

The SML standard library is pretty bare-bones compared to that of other
functional languages, so in a large enough SML project you end up with a
bunch of reimplementations of basic combinators scattered all over the
place. We'd be able to collect them if we had somewhere to collect them,
so here it is.