Many of the definitions and lemmas in `seq_lib.rs`, `set_lib.rs`, `map_lib.rs`, and `multiset.rs` were adapted from the [Dafny standard libraries](https://github.com/dafny-lang/libraries/tree/master/src/Collections), which in turn were assembled from [Ironclad Apps](https://github.com/microsoft/Ironclad/tree/main/ironclad-apps), [IronFleet](https://github.com/microsoft/Ironclad/tree/main/ironfleet), [Vale](https://github.com/project-everest/vale/tree/legacy_dafny), [Verified BetrFS](https://github.com/vmware-labs/verified-betrfs), and [Verifying OpenTitan](https://github.com/secure-foundations/veri-titan).