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 (as₁ ++ as₂) (a₁ :: bs) = reverse as₂ ++ reverseAux as₁ (a₁ :: bs)
no goals