dsimp
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor
      (DVect2.cons f fs))
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (DVect2.cons f fs))
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
as₁ as₂ : List (List α)
a✝ : List α
as✝ : List (List α)
b✝ : List α
bs✝ : List (List α)
f : a✝ ⟶ b✝
fs : DVect2 Quiver.Hom as✝ bs✝
h_ind :
  DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor fs)
    (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor fs)
⊢ DVect2.Eq
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f ++
      Prefunctor.map joinF.toPrefunctor
        (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F)).toPrefunctor fs))
    (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor F).toPrefunctor (f ++ Prefunctor.map joinF.toPrefunctor fs))