∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  j.castSucc < i →
    CategoryTheory.CategoryStruct.comp (X.σ j.castSucc) (X.δ i.succ) =
      CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)