licenses: convert license tags to SPDX

lib: implement instantiate_thm for Trace_Schematic_Insts

This is a function that instantiates a thm with the instantiations provided by
trace_schematic_insts.

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.