dsimp [DVect2.map, DVect2.join]
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq (DVect2.join (DVect2.map (fun a ↦ [a]) (fun a ↦ [a]) (fun {a b} f ↦ DVect2.cons f DVect2.nil) DVect2.nil))
    DVect2.nil
α : Type u
inst✝ : Category α
as bs : List α
⊢ DVect2.Eq DVect2.nil DVect2.nil