This makes f_equiv more powerful: with it we can solve goals of the form f x ≡ g x where f, g: X -d> OFE and f ≡ g. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applies, it will finish the proof, so I added a solve.
I also added the testcases from d16ab1aa.