induction k generalizing bs with
| zero =>
  simp only [Nat.zero_eq, Nat.sub_zero]
  unfold pmapM.map
  exact dif_neg <| Nat.lt_irrefl as.size
| succ k IH =>
  unfold pmapM.map
  rewrite [dif_pos (trans (as.size.sub_succ_lt_self _ hk) (as.size.sub_le k))]
  dsimp [Nat.fold'TR.loop]
  rw [← IH (Nat.le_of_succ_le hk) _]
  apply congrFun; apply congrArg
  rewrite [← Nat.sub_add_comm hk]
  exact Nat.succ_sub_succ_eq_sub as.size k
α : 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
no goals