apply eqF_List <;> dsimp
α : Type u
inst✝ : Category α
⊢ Functor.mk
      { obj := fun X ↦ List.join (List.map (fun a ↦ [a]) X),
        map :=
          fun {X Y} f ↦
            DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f) } =
    Functor.mk { obj := fun X ↦ X, map := fun {X Y} f ↦ f }
case a
α : Type u
inst✝ : Category α
⊢ ∀ (a : List α), List.join (List.map (fun a ↦ [a]) a) = a

case a
α : Type u
inst✝ : Category α
⊢ ∀ (a₁ a₂ : List α) (f : a₁ ⟶ a₂),
    DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) f)) f