## Summary Port [`algebra/lib/mono_list.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/lib/mono_list.v). ## Subtasks - [ ] Lemmas - [ ] Functors ## Dependencies **Rocq dependencies:** - #261 - #252 - #257 - #229 - #231
Summary
Port
algebra/lib/mono_list.v.Subtasks
Dependencies
Rocq dependencies: