reconsider Tr = Tr as DecoratedTree of ;
reconsider v = v as Element of dom Tr ;
Tr . v is type of s ;
hence Tr . v is type of s ; :: thesis: verum