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.