induction l generalizing i with
| nil => cases h; exact List.mem_singleton.mp hfk
| cons k' l IH =>
  cases h with | cons hfk' htail =>
  specialize IH htail (List.not_mem_of_not_mem_cons hk)
  rewrite [List.mem_cons] at hfk
  rewrite [List.mem_cons, not_or] at hk
  cases hfk with
  | inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
  | inr h => exact IH h
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
k : Fin n
hk : ¬k ∈ l
hfk : f k ∈ i :: l
⊢ f k = j
no goals