. intro as₁ as₂ fs
  change DVect2.Eq (DVect2.map id id id fs) fs
  exact DVect2.map_id
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map
        (Prefunctor.obj mapF.toPrefunctor (Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f })).toPrefunctor f)
      f
no goals