∀ (a m j : ℕ),
  j ≤ m →
    ∀ (head : ℕ) (tail : List ℕ),
      (∀ (m : ℕ),
          SimplexCategoryGenRel.IsAdmissible (m + 1) (head :: tail) →
            ∀ j ≤ m, SimplexCategoryGenRel.IsAdmissible m (SimplexCategoryGenRel.simplicialInsert j (head :: tail))) →
        SimplexCategoryGenRel.IsAdmissible (m + 1) (a :: head :: tail) →
          SimplexCategoryGenRel.IsAdmissible m (SimplexCategoryGenRel.simplicialInsert j (a :: head :: tail))