∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (A : Set (Set α))
  (F : (s : Set α) → s ∈ A → C(↑s, β)),
  (∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t),
      (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩) →
    ∀ (i j : { x // x ∈ A }) (x : α) (hxi : x ∈ ↑i) (hxj : x ∈ ↑j), (F ↑i ⋯) ⟨x, hxi⟩ = (F ↑j ⋯) ⟨x, hxj⟩