Expose atomic lifetimes in the API, end many in a single step

This turns out to be useful for my borrow-checker proofs, which require the ability to mass-end lifetimes to model loan termination without generating an inordinate number of laters.

This extracts the proof that atomic lifetimes can end from lft_create_strong as a standalone lemma, and then proves a stronger version of that lemma that terminates arbitrarily many atomic lifetimes at the same time (which is allowed because they don't overlap.) In fact, I think this generalises to being allowed to terminate any number of lifetimes at in the same step, but that requires some more set/multiset theory to prove, I think.

To prove this, I require a few data structure lemmas which I am trying to upstream. Two are going into iris!1049 (merged). The gset_to_map mass-update lemma is harder to generalise - I thought about including it upstream, but it's rather specific here and it doesn't seem to have a nice "kernel" to extract out that would keep the proof burden in these changes small.

added 1 commit

• c02e91ad - Remove upstreamed gset_to_gmap lemmas

Compare with previous version

added 5 commits

• c02e91ad...4691f8dc - 2 commits from branch iris:master
• 127060d7 - Allow ending multiple atomic lfts in a step
• 5f99b57d - Expose atomic lifetimes opaquely in the API
• 66080a2d - Strengthen lft_create to produce atomic lfts

Compare with previous version

added 9 commits

• 66080a2d...72a1c9c3 - 6 commits from branch iris:master
• d077c109 - Allow ending multiple atomic lfts in a step
• 8328c6cd - Expose atomic lifetimes opaquely in the API
• cbcbaf4c - Add lft_create_atomic

Compare with previous version

resolved all threads

added 1 commit

• ff921b62 - Move `lft_kill_atomic` to derived laws

Compare with previous version

resolved all threads

mentioned in commit a97f02f9

merged

Thanks, we can finally land this then :)