induction as
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
as : List α
⊢ forAll p (map f as) = forAll (p ∘ f) as
case nil
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
⊢ forAll p (map f []) = forAll (p ∘ f) []

case cons
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : forAll p (map f tail✝) = forAll (p ∘ f) tail✝
⊢ forAll p (map f (head✝ :: tail✝)) = forAll (p ∘ f) (head✝ :: tail✝)