induction l with
| nil => simp
| cons a l IH =>
  dsimp [pmap]
  simp only [mem_cons, exists_and_left, exists_eq_or_imp, IH]
  apply or_congr_left
  constructor
  . intro h; exact .intro _ h
  . intro h; cases h; assumption
α : Type u
β : Type v
p : α → Prop
b : β
f : (a : α) → p a → β
l : List α
hp : ∀ (a : α), a ∈ l → p a
⊢ b ∈ pmap f l hp ↔ ∃ a h, a ∈ l ∧ b = f a h
no goals