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