`f_equiv` with different functions in head position produces a Leibniz equality
From iris Require Import ofe.
Lemma foo {A C : ofeT} {B : Type} (f g : A -n> B -c> C) (x : A) (y : B) n :
f ≡{n}≡ g → f x y ≡{n}≡ g x y.
Proof.
intros. f_equiv.
This results in f = g
, which cannot be proven.