have : reverseAux as [] = reverse as := rfl
α : Type u_1
p : α → Prop
as bs : List α
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)
α : Type u_1
p : α → Prop
as bs : List α
this : reverseAux as [] = reverse as
⊢ forAll p (reverseAux as bs) = (forAll p as ∧ forAll p bs)