dsimp [DVect2.map, DVect2.join]
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) (DVect2.cons f fs)))
    (DVect2.cons f fs)
α : Type u
inst✝ : Category α
as✝ bs✝ : List α
a : α
as : List α
b : α
bs : List α
f : a ⟶ b
fs : DVect2 Quiver.Hom as bs
h_ind : DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs)) fs
⊢ DVect2.Eq
    (DVect2.cons f DVect2.nil ++
      DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) fs))
    (DVect2.cons f fs)