(rename_i h; simp only [h])
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
no goals