∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (a : α) (b : β)
  (f : α → β → m (ForInStep β)),
  forIn (some a) b f = do
    let r ← f a b
    pure r.value