On Friday, October 13, 2017 at 11:50:40 AM UTC-4, Michael Shulman wrote:

In an ideal world, a judgment x:A |- t:B
would have at most one derivation, so that we could induct on
derivations and still consider the syntactic model to be built out of
terms rather than derivations.

I think this can practically always be arranged. But it's not clear that it actually makes things easier. So I think you might be confused about when and why the interpreter would actually look at derivations.