rw [cons_append, reverseAux, reverseAux, ih]
case cons
α : Type
bs : List α
a✝ b c a : α
as : List α
ih : ∀ (cs : List α), reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs)
cs : List α
⊢ reverseAux (a :: as ++ bs) cs = reverseAux bs (reverseAux (a :: as) cs)
no goals