∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  (o : Option (Option α)) (f : α → β → m (ForInStep β)),
  forIn o.join init f = forIn o init fun o' b => ForInStep.yield <$> forIn o' b f