The list RA has awkward rules for composition due to having to fill up a prefix of the list with "holes" that contain ε. It is barely used (we know of one use by @dkhalanskiyjb); if it were submitted as a new MR nowadays we'd probably just put it into staging, but not accept it into main Iris in its current form.
So this MR "demotes" the list RA to staging. It also adds the lemmas that @dkhalanskiyjb submitted in !371 (closed) (so this MR subsumes !371 (closed)).