dsimp [pmap, pmapM, Nat.fold'TR]
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ pmap f as h = Nat.fold'TR (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[]
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ pmapM.map f as h 0 #[] =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) (size as)
      (_ : Nat.le (size as) (size as)) #[]