refine .cons ?_ IH
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ List.Nodup (f i✝ :: i✝ :: l✝)
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ ∀ (a' : Fin n), a' ∈ i✝ :: l✝ → f i✝ ≠ a'