∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D) (x : SimplexCategoryᵒᵖ)
  (a : CategoryTheory.ComposableArrows C (Opposite.unop x).len),
  (CategoryTheory.nerveMap F).app x a = (F.mapComposableArrows (Opposite.unop x).len).obj a