I think this is the mathematical/logical distinction between "object level" and "meta level". The meta level is about lambda terms, involving things like varia

I think this is the mathematical/logical distinction between "object level" and "meta level". The meta level is about lambda terms, involving things like variable names, abstractions, judgements, derivations, equivalences, reductions, substitutions, etc. The object level is what lambda terms are about, involving things like values, types, variable contents, etc.