f_equiv optimizations

This makes f_equiv a lot faster.

The first commit is inspired by looking at this line in Perennial: the very first f_equiv there takes 30s. 20s of that are spent in simple apply (_ : Proper (R ==> R) f), where f is bi_and <some complicated term> -- basically is tries to treat bi_and as a unary function and takes forever to realize that will not work. There is no TC trace for this, so this must be all unification time. By changing the pattern for this arm from ?R (?f _) _ to ?R (?f _) (?f _) we avoid entering it unless things match syntactically. This seeds up the first f_equiv from 30s to 10s.

The second commit is born from looking at that same line more, and also looking at the equivalent line in Iris itself: according to the ltac profiler, almost all time is spent in try simple apply reflexivity -- again, unification of inequal terms being very slow. So we now do entirely syntactic unification before even trying this. This speeds up the do 23 (f_contractive || f_equiv) in Iris from 1.3s to 0.6s, and it speeds up the do 22 (f_contractive || f_equiv) in Perennial to 0.75s from originally 42s (22s after the previous commit) -- a whopping 50x overall improvement!

Later commits slightly relax this to fix compatibility, so the fallback cases now do perform unification to match up the functions on the left-hand and right-hand side -- but this barely slows down the benchmarks mentioned above since they do not usually hit those cases. In fact, both in the Iris and Perennial case, 66% of the time is now spent in f_contractive.