Discrepancy between f_equal and f_equiv on R x x
From stdpp Require Import tactics.
Lemma test_f_equal_refl {A} (x : A) :
x = x.
Proof. f_equal. Qed.
Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :
R x x.
Proof.
Fail f_equiv.
Abort.
Lemma test {A} (R : relation A) `{!Equivalence R} x :
Proper (R ==> R) (λ _, x).
Proof.
Fail solve_proper.
solve_proper_prepare.
Fail f_equiv. (* R x x, fails similar to above *)
Abort.
The last problem came up in iris!791 (diffs)