∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [ParacompactSpace X] {s : Set X},
  IsClosed s →
    ∀ (u : ι → Set X),
      (∀ (i : ι), IsOpen (u i)) →
        s ⊆ ⋃ i, u i → ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ i, v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i