apply congrFun
case succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
k : Nat
IH :
  ∀ (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
hk : Nat.succ k ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) (push bs (f as[size as - Nat.succ k] (_ : p as[size as - Nat.succ k]))) =
    pmapM.map f as h (size as - k) (push bs (f as[size as - (k + 1)] (_ : p as[size as - (k + 1)])))
case succ.h
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
k : Nat
IH :
  ∀ (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
hk : Nat.succ k ≤ size as
bs : Array β
⊢ pmapM.map f as h (size as - Nat.succ k + 1) = pmapM.map f as h (size as - k)