mathbox: improvements, glossary and eliminability

[wlammen]

• start adding a glossary with frequently used terms
• apply the words from the glossary consistently
• explain eliminability on a separate page
• point out the role of implicit substitution for auxiliary axioms
• improve formatting in some cases
• delete obsolete htmldefs overdue for 6 years. May be there are more leftovers after definitions were removed. Need to check this.

IMO mmset.raw.html needs an update.

• The term "closed form" is nowhere introduced, as opposed to "inference form"
• Meantime main has more than 30000 theorems. The last theorem is pliguhgr.
• Certain topics like eliminability of classes are not sufficient
• Some information is scattered in several positions

[icecream17]

impressive analysis, never realized that

[jkingdon]

Agreed. Metamath notation makes it easy for us to not distinguish whether a proposition contains any classes or whether it just contains setvars. But when we are talking about something like whether classes could in principle be eliminated, it is valuable to be aware of this.