cases h
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
hfa : a'✝ ∈ i✝ :: l✝
h : f i✝ = a'✝
⊢ False
case cons.refl
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✝)
hfa : f i✝ ∈ i✝ :: l✝
⊢ False