∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂),
  CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 (CategoryTheory.ComposableArrows.mk₂ f g) =
    CategoryTheory.ComposableArrows.mk₁ g