Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinalsby Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel12 Nov