∀ (m : ℕ) (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L ↔
    L = [] ∨
      (∃ a ≤ m, L = [a]) ∨
        ∃ a b L', a < b ∧ SimplexCategoryGenRel.IsAdmissible (m + 1) (b :: L') ∧ a ≤ m ∧ L = a :: b :: L'