This doesn't need to be part of the signature (and in fact, I just
derived it directly from `lft_kill_atomics` when I proved it,) so it's
now explicitly a derived law to keep the signature minimal.

This lemma exposes the fact that `lft_create` can be used to actually
produce an atomic lifetime. This version of the lemma doesn't need to
include the killing update thanks to the existence of `lft_kill_atomic`
which is always applicable for these atomic lifetimes.

This *could* replace `lft_create`, but we keep that lemma for backwards
compatibility in the API.

This extends the lifetime signature to expose the notion of atomic
lifetimes and how they can embed into normal lifetimes. This allows for
a future lemma where I will state that a particular new lifetime is
atomic, thus allowing for the application of the lifetime-ending lemma
at a later point.

This has been done opaquely rather than exposing directly the definition
of `atomic_lft` to try to keep the API clean.

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.