f ≡ g doesn’t imply f x ≡ g x for an arbitrary ≡, even tho it does for yours. My usual fix for such issues would give rewrite (EQ _ _) here, but that assumes the following definition for eq_rel.
Definition eq_rel {A B} (R : A -> B -> Prop) (S : A -> B -> Prop) :=
forall (x : A) (y : B), R x y <-> S x y.
I’ve run into similar issues before and discussed them in: Extensional setoids on functions, and rewriting.