∀ {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((_ : α) × β)} {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  (forIn l init fun a d => f a.fst a.snd d) = forIn (List.map (fun x => (x.fst, x.snd)) l) init fun a d => f a.1 a.2 d