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