simp [all, all', List.foldr, List.map, ih]
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ all p (a::as) = all' p (a::as)
case cons
α : Sort u_1
p : α → Bool
a : α
as : List α
ih : all p as = all' p as
⊢ (p a && List.foldr and true (List.map p as)) = (p a && all' p as)