suffices ∀ (k : Nat) (hk : k ≤ as.size) (bs : Array β), pmapM.map (m:=Id) f as h (as.size - k) bs = Nat.fold'TR.loop as.size _ k hk bs
from Eq.trans (as.size.sub_self ▸ rfl) (this as.size .refl #[])
α : 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)) #[]
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
⊢ ∀ (k : Nat) (hk : k ≤ size as) (bs : Array β),
    pmapM.map f as h (size as - k) bs =
      Nat.fold'TR.loop (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) k hk bs