∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] (n : ℕ)
  {f g : (CategoryTheory.nerve C).obj (Opposite.op (SimplexCategory.mk (n + 1)))},
  (CategoryTheory.nerve C).map (SimplexCategory.mkOfSucc 0).op f =
      (CategoryTheory.nerve C).map (SimplexCategory.mkOfSucc 0).op g →
    CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 f =
        CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 g →
      f = g