no goals
ι : Type ?u.26992
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
⊢ concat l a = reverse (a :: reverse l)
simp only [concat_eq_append, reverse_cons, reverse_reverse]