Start working on semantics of subst/inst

Copy all the de Bruijn and freshly renamed terms stuff across, as well
as simple_inst and simple_subst, and prove a theorem about the semantics
of simple_subst. This actually involves a lot more code than Harrison's
original proofs (even though the results are basically the same): not
sure if it's worth it; the advantage is the proofs are somewhat less
complicated this way albeit more numerous.

This stuff is still really annoyingly fiddly, and a lot of it is because
of the stupid representation of substitutions/instantiations (as lists
of terms or types), and because there's not great support for updating
functions (unlike updating finite maps). I haven't switched to a better
representation (e.g. finite maps) this time, because I wanted to avoid
having to switch back and forth between them...