Allow ending multiple atomic lfts in a step

This turns out to probably be useful for my borrow-checker proofs, which
require the ability to mass-end lifetimes to model loan termination.

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.)

To prove this, I require a few data structure lemmas which I am trying
to upstream to Iris.