## Summary Port [`algebra/max_prefix_list.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/max_prefix_list.v). ## Subtasks - [ ] Lemmas - [ ] Functors ## Dependencies **Rocq dependencies:** - #226 - #254 - #221 - #229 - #231
Summary
Port
algebra/max_prefix_list.v.Subtasks
Dependencies
Rocq dependencies: