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