no goals
α : Type u_1
β : Type ?u.440899
γ : Type ?u.440902
δ : Type ?u.440905
r : α → β → Prop
p : γ → δ → Prop
s t : Multiset α
⊢ Rel (flip fun x x_1 => x = x_1) s t ↔ s = t
rw [rel_flip, rel_eq, eq_comm]