Refactor to remove Eq_result type

It's unnecessary and doesn't make code much clearer.
It can be replaced with bool option. The advantage of using option is that do_eq_list can be written using OPT_MMAP or maybe a new defined higher order function and there's no need mutual recursive functions for do_eq. Setting up similar definitions and proofs for Eq_result is not worth it.