∀ {α : Type u_2} {β : Type u_3} {ι : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} (u : Set (β × β))
  (motive : (∃ x, UniformContinuousOn (F x) s ∧ ∀ x_1 ∈ s, (f x_1, F x x_1) ∈ u) → Prop)
  (x : ∃ x, UniformContinuousOn (F x) s ∧ ∀ x_1 ∈ s, (f x_1, F x x_1) ∈ u),
  (∀ (i : ι) (hF : UniformContinuousOn (F i) s ∧ ∀ x ∈ s, (f x, F i x) ∈ u), motive ⋯) → motive x