∀ {m : Type w → Type w'} [inst : Monad m] {α β : Type w} {x : Std.Iterators.PostconditionT m α}
  {f : α → Std.Iterators.PostconditionT m β},
  (x >>= f).operation = do
    let a ← x.operation
    (fun fa => ⟨↑fa, ⋯⟩) <$> (f ↑a).operation