∀ {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p x → Prop} {b : Prop},
  (∃! x, ∃! h, q x h) → (∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) → b