rw [reverseAux_eq_append, forAll_append, this, forAll_reverse]
α : Type u_1
p : α → Prop
as bs : List α
this : reverseAux as [] = reverse as
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)
no goals