∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} [inst_1 : Monad n] [LawfulMonad n]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β}
  {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)},
  forIn (Std.Iter.filter f it) init g =
    forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc)