∀ (α : Type u_2) (β : Type u_1) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (s : Set (C(α, β) × C(α, β)))
  (motive :
    (∃ i,
        (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
          {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s) →
      Prop)
  (x :
    ∃ i,
      (IsCompact i.1 ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧ {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ i.2} ⊆ s),
  (∀ (a : Set α) (b : Set (β × β)) (left : IsCompact (a, b).1) (ε : ℝ) (hε : 0 < ε)
      (hb : {p | dist p.1 p.2 ≤ ε} ⊆ (a, b).2) (hs : {fg | ∀ x ∈ (a, b).1, (fg.1 x, fg.2 x) ∈ (a, b).2} ⊆ s),
      motive ⋯) →
    motive x