. intro ass
  induction ass
  case a.nil => rfl
  case a.cons as ass h_ind =>
    dsimp at *
    have : ∀ (as bs : List α), (mapF.obj F).obj (as++bs) = (mapF.obj F).obj as ++ (mapF.obj F).obj bs :=
      λ as bs => List.map_append F.obj _ _
    rw [this, h_ind]
case a
α : Type u
inst✝¹ : Category α
β : Type v
inst✝ : Category β
F : α ⥤ β
⊢ ∀ (a : List (List α)),
    Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor (Prefunctor.obj mapF.toPrefunctor F) ⋙ joinF).toPrefunctor a =
      Prefunctor.obj (joinF ⋙ Prefunctor.obj mapF.toPrefunctor F).toPrefunctor a

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)
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)