∀ {ι : Sort u_1} {c : ι → Set ↑unitInterval},
  (∀ (i : ι), IsOpen (c i)) →
    Set.univ ⊆ ⋃ i, c i →
      ∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i