induction h with
| single => exact .cons (fun _ h => nomatch h) .nil
| cons hnotmem _ IH =>
  refine .cons ?_ IH
  intro _ hfa h; cases h
  exact hnotmem hfa
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
⊢ List.Nodup (i :: l)
no goals