∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X}
  (motive : (∃ v, Set.univ ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i) → Prop)
  (x : ∃ v, Set.univ ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i),
  (∀ (v : ι → Set X) (vU : Set.univ ⊆ Set.iUnion v) (hv : (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i),
      motive ⋯) →
    motive x