rfl
α : Type u
inst✝ : Category α
a✝ b✝ c✝ : α
as✝ bs✝ cs✝ : List α
f✝ : a✝ ⟶ b✝
fs✝ : Hom as✝ bs✝
g✝ : b✝ ⟶ c✝
gs✝ : Hom bs✝ cs✝
⊢ List.comp (DVect2.cons f✝ fs✝) (DVect2.cons g✝ gs✝) = DVect2.cons (f✝ ≫ g✝) (List.comp fs✝ gs✝)
no goals