. intros as₁ as₂ fs
  induction fs
  case a.nil => exact DVect2.Eq.nil_rfl
  case a.cons f fs h_ind =>
    dsimp
    have : ∀ {as₁ as₂ bs₁ bs₂ : List α} (fs₁ : as₁ ⟶ bs₁) (fs₂ : as₂ ⟶ bs₂), DVect2.Eq ((mapF.obj F).map (fs₁ ++ fs₂)) ((mapF.obj F).map fs₁ ++ (mapF.obj F).map fs₂) :=
      λ fs₁ fs₂ => DVect2.map_append F.obj F.obj F.map
    apply DVect2.Eq.trans _ (this f (joinF.map fs)).symm
    apply DVect2.eq_of_eq_append_eq (DVect2.Eq.of rfl) h_ind
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a₁ a₂ : List (List α)) (f : a₁ ⟶ a₂),
    DVect2.Eq
      (Prefunctor.map (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor f)
      (Prefunctor.map (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor f)
no goals