Theorem: List.forAll_reverseAux (Algdata/Data/List/Prop.lean)

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

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