induction l with
| nil => rfl
| cons a l IH => dsimp [pmap]; rw [IH]
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
⊢ length (pmap f l h) = length l
no goals