induction as₁ <;> intro bs
α : Type u
β : Type v
γ : Type w
as₁ as₂ : List α
⊢ ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
case nil
α : Type u
β : Type v
γ : Type w
as₂ bs : List α
⊢ reverseAux ([] ++ as₂) bs = reverse as₂ ++ reverseAux [] bs

case cons
α : Type u
β : Type v
γ : Type w
as₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {bs : List α}, reverseAux (tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux tail✝ bs
bs : List α
⊢ reverseAux (head✝ :: tail✝ ++ as₂) bs = reverse as₂ ++ reverseAux (head✝ :: tail✝) bs