∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)},
  forIn (List.map g l) init f = forIn l init fun a y => f (g a) y