∀ {α : Type u_1} (r : α → α → Prop) (a b : List α),
  (List.IsRotated.setoid α) a b →
    (match a with
      | [] => True
      | a :: m => List.IsChain r (a :: m ++ [a])) =
      match b with
      | [] => True
      | a :: m => List.IsChain r (a :: m ++ [a])