revert bs
α : Type u
β : Type v
γ : Type w
as₁ as₂ bs : List α
⊢ reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs