no goals
ι : Type ?u.132558
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
a : α
l : List α
⊢ map f (concat l a) = concat (map f l) (f a)
induction l <;> [rfl; simp only [*, concat_eq_append, cons_append, map, map_append]]