∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {u : β → α} (motive : (∃ b, ∀ (x : β), r (u x) b) → Prop)
  (x : ∃ b, ∀ (x : β), r (u x) b), (∀ (b : α) (hb : ∀ (x : β), r (u x) b), motive ⋯) → motive x