α : Type u
β : Type v
γ : Type w
as : List α
⊢ reverseAux (reverseAux as nil) nil = as
α : Type u
β : Type v
γ : Type w
as : List α
⊢ reverse (reverse as) = as
simp [reverse]
α : Type u
β : Type v
γ : Type w
as : List α
⊢ reverseAux nil as = as
α : Type u
β : Type v
γ : Type w
as : List α
⊢ reverseAux (reverseAux as nil) nil = as
rw [reverseAux_reverseAux_nil]
no goals
α : Type u
β : Type v
γ : Type w
as : List α
⊢ reverseAux nil as = as
rfl