∀ {n : SimplexCategory} (f g : SimplexCategory.mk 1 ⟶ n),
  autoParam ((SimplexCategory.Hom.toOrderHom f) 0 = (SimplexCategory.Hom.toOrderHom g) 0)
      SimplexCategory.Hom.ext_one_left._auto_1 →
    autoParam ((SimplexCategory.Hom.toOrderHom f) 1 = (SimplexCategory.Hom.toOrderHom g) 1)
        SimplexCategory.Hom.ext_one_left._auto_3 →
      f = g