∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {p : α → Prop} {q : β → Prop}
  (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) (b : { b // q b }), ↑((e.subtype h).symm b) = e.symm ↑b