α : Type u
β : Type v
γ : Type w
a : α
as : List α
⊢ reverseAux as (a :: nil) = reverseAux as nil ++ a :: nil
α : Type u
β : Type v
γ : Type w
a : α
as : List α
⊢ reverse (a :: as) = reverse as ++ a :: nil
simp [reverse, reverseAux]
no goals
α : Type u
β : Type v
γ : Type w
a : α
as : List α
⊢ reverseAux as (a :: nil) = reverseAux as nil ++ a :: nil
rw [← reverseAux_eq_append]