Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.

This solves issue #161 (closed)

mentioned in merge request iris!791 (merged)

@jung Would be great to run CI here to see if this does not break anything.

I vaguely remember not using reflexivity because it can be very slow...

... oh but you did something slightly different, interesting. We already have fast_done, should (a) those two be placed together and (b) fast_done call fast_reflexivity?

added 1 commit

• 6aa72baa - Apply 2 suggestion(s) to 2 file(s)

Compare with previous version

added 1 commit

• ba3c17be - make sure this solves the goal

Compare with previous version

added 1 commit

• 9236a721 - Move.

Compare with previous version

resolved all threads

Ok, so pending a CI run, this is ready I think.

The CI run did not find any breakage.

merged

mentioned in commit ffa862a8

mentioned in issue #161 (closed)