∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α),
  (List.IsRotated.setoid α) l₁ l₂ →
    ∀ (h₁ : Cycle.Nodup (Quot.mk (⇑(List.IsRotated.setoid α)) l₁))
      (h₂ : Cycle.Nodup (Quot.mk (⇑(List.IsRotated.setoid α)) l₂)) (x y : α),
      x ≍ y →
        ∀ (hm : x ∈ Quot.mk (⇑(List.IsRotated.setoid α)) l₁) (hm' : y ∈ Quot.mk (⇑(List.IsRotated.setoid α)) l₂),
          hm ≍ hm' → (fun l _hn x hx => l.next x hx) l₁ h₁ x hm = (fun l _hn x hx => l.next x hx) l₂ h₂ y hm'