apply eqF_List
α : Type u
inst✝ : Category α
⊢ Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α),
    Prefunctor.obj (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor a =
      Prefunctor.obj (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X ++ [], map := fun {X Y} f ↦ f ++ DVect2.nil }).toPrefunctor f)
      (Prefunctor.map (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }).toPrefunctor f)