induction l with
| nil => exact i.elim0
| cons a l IH =>
  let ⟨i,hi⟩ := i
  cases i <;> dsimp; rfl
  exact IH _ _
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
i : Fin (length (pmap f l h))
⊢ get (pmap f l h) i =
    f (get l (Fin.cast (_ : length (pmap f l h) = length l) i))
      (_ : p (get l (Fin.cast (_ : length (pmap f l h) = length l) i)))
no goals