In the course of writing the bedrock2 backend for fiat-crypto, I ended up needing several lemmas that were not at all specific to the task, and instead were more basic facts about lists, sets, maps, etc. This PR upstreams the generalizable list lemmas.
In the course of writing the bedrock2 backend for fiat-crypto, I ended up needing several lemmas that were not at all specific to the task, and instead were more basic facts about lists, sets, maps, etc. This PR upstreams the generalizable list lemmas.