case cons a₁ as₁ h_ind =>
  rw [cons_append]
  unfold reverseAux
  rw [h_ind]
α : Type u
β : Type v
γ : Type w
as₂ : List α
a₁ : α
as₁ : List α
h_ind : ∀ {bs : List α}, reverseAux (as₁ ++ as₂) bs = reverse as₂ ++ reverseAux as₁ bs
bs : List α
⊢ reverseAux (a₁ :: as₁ ++ as₂) bs = reverse as₂ ++ reverseAux (a₁ :: as₁) bs
no goals