∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] [inst_8 : Std.Iterator α m β] [inst_9 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β},
  (Std.IterM.flatMap f it₁).toList = List.flatten <$> (Std.IterM.mapM (fun b => (f b).toList) it₁).toList