Refactor to remove Eq_result type

[ordinarymath]

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.

[tanyongkiam]

I'm not sure this is a necessary refactor. In particular, I don't think I agree that using OPT_MMAP or using the list recursor is necessarily better.