conv =>
  rhs
  rw [DVect2.cons_append]
  dsimp
  rw [Category.id_comp]
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      ((Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (𝟙 (Prefunctor.obj F.toPrefunctor a✝)) (appendF.naturatorLax F as✝ as₂) ≫
      Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs ++ gs)
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ bs₁ bs₂ : List α
gs : as₂ ⟶ bs₂
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
        Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
      appendF.naturatorLax F bs✝ bs₂ =
    appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs)
⊢ DVect2.cons (Prefunctor.map F.toPrefunctor f)
      ((Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs ++
          Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor gs) ≫
        appendF.naturatorLax F bs✝ bs₂) =
    DVect2.cons (Prefunctor.map F.toPrefunctor f)
      (appendF.naturatorLax F as✝ as₂ ≫ Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (fs ++ gs))