unfold pmapM.map
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as) bs = Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
hk : Nat.zero ≤ size as
bs : Array β
⊢ (if hlt : size as < size as then do
      let __do_lift ← f as[size as] (_ : p as[size as])
      pmapM.map f as h (size as + 1) (push bs __do_lift)
    else pure bs) =
    Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) 0 hk bs