∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → Option β'} {p : β' → Bool},
  Std.Iter.all p (Std.Iter.filterMap f it) =
    Std.Iter.all
      (fun x =>
        match f x with
        | some fx => p fx
        | none => true)
      it