∀ {α : Type u_2} [inst : PseudoMetricSpace α] {β : Type u_1} {p : β → Prop} {f : β → ℝ} (s : Set (α × α))
  (motive : (∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s) → Prop) (x : ∃ i, p i ∧ {p | dist p.1 p.2 < f i} ⊆ s),
  (∀ (i : β) (hi : p i) (H : {p | dist p.1 p.2 < f i} ⊆ s), motive ⋯) → motive x