Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel Nov 12