The derivability of a given statement can be justified by exhibiting a derivation tree [...] For example, if
[ some definitions ]
then the derivability of the statement
if t then false else false --> if u then false else false
is witnessed by the following derivation tree:
(Types and Programming Languages by Benjamin C. Pierce)
Does witnessed here means the same as is justified from above?
More examples from the same book:
Indeed, the derivation trees witnessing evaluation statements will always have this slender form: since no evaluation rule has more than one premise, there is no way to construct a branching derivation tree.
In the simple type system we are dealing with in this chapter, every term has a single type (if it has any type at all), and there is always just one derivation tree witnessing this fact.