Skip to content

Generalize `list_find` lemmas to become bi-implications.

Robbert Krebbers requested to merge robbert/list_find into master

Thanks to @jules for the suggestion and an initial proof.

PS: I moved the block of code down because it now depends on some of the Forall lemmas that only appear later in the list.v file.

Edited by Robbert Krebbers

Merge request reports