case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
⊢ formPerm (reverse (Quot.mk Setoid.r a✝)) (_ : Nodup (reverse (Quot.mk Setoid.r a✝))) =
    (formPerm (Quot.mk Setoid.r a✝) h)⁻¹
α : Type u_1
inst✝ : DecidableEq α
s✝ s' s : Cycle α
h : Nodup s
⊢ formPerm (reverse s) (_ : Nodup (reverse s)) = (formPerm s h)⁻¹
induction s using Quot.inductionOn
no goals
case h
α : Type u_1
inst✝ : DecidableEq α
s s' : Cycle α
a✝ : List α
h : Nodup (Quot.mk Setoid.r a✝)
⊢ formPerm (reverse (Quot.mk Setoid.r a✝)) (_ : Nodup (reverse (Quot.mk Setoid.r a✝))) =
    (formPerm (Quot.mk Setoid.r a✝) h)⁻¹
simpa using formPerm_reverse _ h