∀ {S : SSet} {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc)
  (x : S.obj (Opposite.op (SimplexCategory.mk (n + 2)))),
  CategoryTheory.SimplicialObject.δ S (i.castLT ⋯) (CategoryTheory.SimplicialObject.δ S j.succ x) =
    CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.δ S i x)