∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc) {Z : C} (h : X.obj (SimplexCategory.mk (n + 1 + 1)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.δ (i.castLT ⋯)) (CategoryTheory.CategoryStruct.comp (X.δ j.succ) h) =
    CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ i) h)