induction as
α : Type u_1
p : α → Prop
as bs : List α
⊢ forAll p (as ++ bs) = (forAll p as ∧ forAll p bs)
case nil
α : Type u_1
p : α → Prop
bs : List α
⊢ forAll p ([] ++ bs) = (forAll p [] ∧ forAll p bs)

case cons
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)