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, which in turn were assembled from Ironclad Apps, IronFleet, Vale, Verified BetrFS, and Verifying OpenTitan.