∀ (L : List ℕ) (j : ℕ),
  SimplexCategoryGenRel.simplicialEvalσ L j =
    match L with
    | [] => j
    | a :: L =>
      if a < SimplexCategoryGenRel.simplicialEvalσ L j then SimplexCategoryGenRel.simplicialEvalσ L j - 1
      else SimplexCategoryGenRel.simplicialEvalσ L j