no goals
α : Type u
β : Type v
γ : Type w
as bs cs : List α
⊢ reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as nil) cs)
induction as generalizing bs cs with
| nil => rfl
| cons a as ih => simp [reverseAux, ih (a::bs), ih [a]]
no goals
case nil
α : Type u
β : Type v
γ : Type w
bs cs : List α
⊢ reverseAux (reverseAux nil bs) cs = reverseAux bs (reverseAux (reverseAux nil nil) cs)
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : ∀ (bs cs : List α), reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as nil) cs)
bs cs : List α
⊢ reverseAux (reverseAux (a :: as) bs) cs = reverseAux bs (reverseAux (reverseAux (a :: as) nil) cs)
simp [reverseAux, ih (a::bs), ih [a]]