∀ {α : Type u_1} {σ : Type u_2} (F : Ctop α σ) {s : Set α} {a : α}
  (motive : (∃ t ∈ Set.range F.f, a ∈ t ∧ t ⊆ s) → Prop) (x : ∃ t ∈ Set.range F.f, a ∈ t ∧ t ⊆ s),
  (∀ (x : σ) (h : a ∈ F.f x ∧ F.f x ⊆ s), motive ⋯) → motive x