f_equiv: slightly better support for function relations
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
I also added the testcases from d16ab1aa.