∀ {n : ℕ} (i : Fin (n + 1)) (i' : Fin (n + 2)),
  ∃ z e m,
    ∃ (_ : SimplexCategoryGenRel.P_σ e) (_ : SimplexCategoryGenRel.P_δ m),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i') (SimplexCategoryGenRel.σ i) =
        CategoryTheory.CategoryStruct.comp e m