∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m (Option γ)} (it : Std.IterM Id β),
  (Std.IterM.filterMapWithPostcondition f it).toArray = Array.filterMapM (fun x => (f x).run) it.toArray.run