∀ {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [inst : Monad m] (as : Batteries.RBNode α) (init : σ)
  (f : α → σ → m (ForInStep σ)), as.forIn init f = ForInStep.run <$> Batteries.RBNode.forIn.visit f as init