∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (p : X.Path (n + 1)),
  SSet.StrictSegalCore.spineToSimplex h p =
    (h n).concat (p.arrow 0) (SSet.StrictSegalCore.spineToSimplex h (p.interval 1 n ⋯)) ⋯