Remove funext from isequiv_O_prod_cmp

It's unneeded.

This commit also automates some of the functoriality proofs a bit more.

The tactic `reflective_subuniverse_functor_rewrite_under_binders_t` is a prime example of where setoid automation could help; we could declare that `O_rectnd` respects homotopies, and then `setoid_rewrite` with any theorem that ends in a homotopy.