. intro as₁ as₂ fs
  exact DVect2.map_comp
case a
α : Type u
inst✝² : Category α
β : Type v
inst✝¹ : Category β
γ : Type w
inst✝ : Category γ
F : α ⥤ β
G : β ⥤ γ
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (DVect2.map (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun X ↦ Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor X))
        (fun {a b} f ↦ Prefunctor.map G.toPrefunctor (Prefunctor.map F.toPrefunctor f)) f)
      (DVect2.map G.toPrefunctor.obj G.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map G.toPrefunctor)
        (DVect2.map F.toPrefunctor.obj F.toPrefunctor.obj (fun {a b} ↦ Prefunctor.map F.toPrefunctor) f))
no goals