attempt to prove semantics_has_meaning

not true, but for a possibly silly reason.
it seems it might be better if free bound de Bruijn variables also
carried their types... (bound in context as opposed to in the term; this
would mean being able to see whether the term type-checks without the
context..)