∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ} {s : Set X},
  IsPathConnected s →
    ∀ (p : Fin (n + 1) → X),
      (∀ (i : Fin (n + 1)), p i ∈ s) → ∃ γ t, (∀ (t : ↑unitInterval), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i