dsimp [forAll]
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ forAll p (head✝ :: tail✝ ++ bs) = (forAll p (head✝ :: tail✝) ∧ forAll p bs)
α : Type u_1
p : α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : forAll p (tail✝ ++ bs) = (forAll p tail✝ ∧ forAll p bs)
⊢ (p head✝ ∧ forAll p (tail✝ ++ bs)) = ((p head✝ ∧ forAll p tail✝) ∧ forAll p bs)