∀ {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    ∀ {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk (n + 1 + 1) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc) h)