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.