Begin a theory of 'hereditarily finite bags'.

Inspired by a conversation with Jasmin Blanchette, and also

https://www.isa-afp.org/entries/Nested_Multisets_Ordinals.shtml