[endgame]

> How can we print this in such a way that preserves semantics?

Maybe try something like normalisation-by-evaluation, but if you go to look up a free variable, replace that lookup with a little bit of syntax tree instead?