case intro
α : Type u_1
β : Type ?u.774035
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hd : Nodup l
n : ℕ
⊢ formPerm l = formPerm (rotate l n)
α : Type u_1
β : Type ?u.774035
inst✝ : DecidableEq α
l✝ : List α
x : α
l l' : List α
hd : Nodup l
h : l ~r l'
⊢ formPerm l = formPerm l'
obtain ⟨n, rfl⟩ := h
no goals
case intro
α : Type u_1
β : Type ?u.774035
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
hd : Nodup l
n : ℕ
⊢ formPerm l = formPerm (rotate l n)
exact (formPerm_rotate l hd n).symm