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
case cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
IH : ∀ {i : Fin n}, OrbitChain f i l j → ¬k ∈ l → f k ∈ i :: l → f k = j
i : Fin n
h : OrbitChain f i (k' :: l) j
hk : ¬k ∈ k' :: l
hfk : f k ∈ i :: k' :: l
⊢ f k = j
no goals