Generalize `list_find` lemmas to become bi-implications.
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