no goals
ι : Type ?u.324787
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Prop
f : α → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap (fun a x => f a) l H = map f l
induction l <;> [rfl; simp only [*, pmap, map]]