∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : γ) (x_3 : α) (xr : List α)
  (y : β) (yr : List β),
  List.mapAccumr₂ f (x_3 :: xr) (y :: yr) x =
    ((f x_3 y (List.mapAccumr₂ f xr yr x).1).1,
      (f x_3 y (List.mapAccumr₂ f xr yr x).1).2 :: (List.mapAccumr₂ f xr yr x).2)