This closes #391. It depends on stdpp!239 (merged).
This adds an RA max_listR for lists where composition is only valid if one list is a prefix of the other, a derived RA mono_listR using auth that only allows lists to grow by appending, and a set of logic-level assertions for mono_list.
The logic-level assertions are:
- an authoritative assertion for the full list
- a persistent assertion for some list which is a prefix of the auth list
- a persistent ownership that index i in the auth list is some particular value.
This, to my understanding after some inspection, should support the needs of the various versions mentioned in #391.