This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.