case cons a as h_ind =>
  dsimp [forAll]
  rw [h_ind, And.comm, and_true]
α : Type u_1
p : α → Prop
a : α
as : List α
h_ind : forAll p (reverse as) = forAll p as
⊢ forAll p (reverse as) ∧ forAll p [a] ↔ forAll p (a :: as)
no goals