cases h
case nil
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k i : Fin n
h : OrbitChain f i [] j
hk : ¬k ∈ []
hfk : f k ∈ [i]
⊢ f k = j
case nil.single
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k : Fin n
hk : ¬k ∈ []
hfk : f k ∈ [j]
⊢ f k = j