case cons a as h_ind =>
  dsimp
  rw [DVect2.cons_append, h_ind]
α : Type u
inst✝ : Category α
bs : List α
a : α
as : List α
h_ind : 𝟙 as ++ 𝟙 bs = 𝟙 (as ++ bs)
⊢ 𝟙 (a :: as) ++ 𝟙 bs = 𝟙 (a :: as ++ bs)
no goals