dsimp
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ List.join (List.map (fun a ↦ [a]) (a :: as)) = a :: as
α : Type u
inst✝ : Category α
a : α
as : List α
h_ind : List.join (List.map (fun a ↦ [a]) as) = as
⊢ a :: List.join (List.map (fun a ↦ [a]) as) = a :: as