∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α₁ → α₂} {g : α₂ → β → m β} {as : List α₁},
  List.scanrM g init (List.map f as) = List.scanrM (fun a b => g (f a) b) init as