press on with semantics of de Bruijn terms

despite not having been able to prove much interesting about them.
want to see what is actually required for the semantics and soundness to
go through.
have updated the semantics to be on de Bruijn terms and proved that it's
still one-to-one (and that proof no longer uses INST_CORE_HAS_TYPE).