Ah, yeah, for setoids you are going to want to prove something more general, just that there exists some proof that makes them equal, rather than insisting it's ≈refl.