congr for unions

Stream: general

[Yury G. Kudryashov]

The following example fails:

import data.set.lattice

example (α β : Type*) (p q : α → Prop) (h : ∀ x, p x ↔ q x) (s : α → set β) :
  (⋃ (x : α) (hx : p x), s x) = ⋃ (x : α) (hx : q x), s x :=
by simp [h]

How can we make it work?

[Yury G. Kudryashov]

I guess that we need some congr lemma for Union but I'm not sure how exactly should it look like.