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.