∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D) {x y : C} (f : x ⟶ y),
  (CategoryTheory.nerveMap F).app (Opposite.op (SimplexCategory.mk 1)) (CategoryTheory.ComposableArrows.mk₁ f) =
    CategoryTheory.ComposableArrows.mk₁ (F.map f)