. intro as bs fs
  induction fs
  case a.nil =>
    dsimp [DVect2.map, DVect2.join]
    exact DVect2.Eq.of rfl
  case a.cons a as b bs f fs h_ind =>
    dsimp [DVect2.map, DVect2.join]
    rw [DVect2.cons_append, DVect2.nil_append]
    exact DVect2.Eq.descend rfl h_ind
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
no goals