Footnotes

 

(1)

The notion of explicitly-sorted term is redundant in the many-sorted framework, but becomes significant when subsorts are introduced in a later section.