mathbox: improvements, glossary and eliminability (#5055)

* fixes, role of implicit sustitution for auxiliary axioms

* improvements and explain eliminability

* fixes

* more fixes

* improvements suggested by SN

* fix a date

* typo

* add a link suggested by TA

Author: wlammen