∀ (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁) {Z : SimplexCategoryGenRel}
  (h_1 : SimplexCategoryGenRel.mk m₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ (a :: L) h) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L ⋯)
      (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a)) h_1)