∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (t : ↑unitInterval),
  ∀ x_1 ∈ {Path.refl x},
    { toFun := fun x_2 => (fun p => Path.delayReflLeft p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
      ({ toFun := fun ρ => ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
          ((ContinuousMap.const (Path x x) (Path.refl x)).prodMk (ContinuousMap.id (Path x x))))
        x_1