rw [DVect2.cons_append, DVect2.cons_append]
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ (DVect2.cons f fs₁ ++ fs₂) ≫ (DVect2.cons g gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂
α : Type u
inst✝ : Category α
head✝² : α
tail✝² x✝² : List α
head✝¹ : α
tail✝¹ x✝¹ : List α
head✝ : α
tail✝ x✝ : List α
f : head✝² ⟶ head✝¹
fs₁ : DVect2 Quiver.Hom tail✝² tail✝¹
fs₂ : Hom x✝² x✝¹
g : head✝¹ ⟶ head✝
gs₁ : DVect2 Quiver.Hom tail✝¹ tail✝
gs₂ : Hom x✝¹ x✝
⊢ DVect2.cons f (fs₁ ++ fs₂) ≫ DVect2.cons g (gs₁ ++ gs₂) = DVect2.cons f fs₁ ≫ DVect2.cons g gs₁ ++ fs₂ ≫ gs₂