{X : Type u_1} →
  [inst : TopologicalSpace X] →
    {n : ℕ} →
      (p : Fin (n + 1) → X) →
        (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
          ((k : Fin n) → (F k).Homotopy (G k)) → (Path.concat p F).Homotopy (Path.concat p G)