more work on semantics

not obviously making progress, but going back and forth a lot, which is
worrying. might be due for a cleanup. using finite maps everywhere and
de Bruijn indices does mean that everything is very explicit (and hence
means book-keeping). but it's still not clear that this actually solves
the difficulties with instantiation and substitution.