α : Type u_1
l : List α
a : α
⊢ reverse [a] ++ reverse l = a :: reverse l
α : Type u_1
l : List α
a : α
⊢ reverse (concat l a) = a :: reverse l
rw [concat_eq_append, reverse_append]
no goals
α : Type u_1
l : List α
a : α
⊢ reverse [a] ++ reverse l = a :: reverse l
rfl