induction fs
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
fs : as₁ ⟶ bs₁
gs : as₂ ⟶ bs₂
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs) ≫ appendF.naturatorOplax F bs₁ bs₂ =
    appendF.naturatorOplax F as₁ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
case nil
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.nil ++ gs) ≫
      appendF.naturatorOplax F [] bs₂ =
    appendF.naturatorOplax F [] as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor DVect2.nil ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)

case cons
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝² : α
as✝ : List α
b✝ : α
bs✝ : List α
a✝¹ : a✝² ⟶ b✝
a✝ : DVect2 Quiver.Hom as✝ bs✝
a_ih✝ :
  Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (a✝ ++ gs) ≫ appendF.naturatorOplax F bs✝ bs₂ =
    appendF.naturatorOplax F as✝ as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a✝ ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)
⊢ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝ ++ gs) ≫
      appendF.naturatorOplax F (b✝ :: bs✝) bs₂ =
    appendF.naturatorOplax F (a✝² :: as✝) as₂ ≫
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons a✝¹ a✝) ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs)