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.