simp only [List.mem_cons, not_or] at h
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
h : ¬i = j ∧ ¬i ∈ k :: l
y : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
IH : ¬i = j ∧ ¬i ∈ l → ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
⊢ (List.foldr (fun j_1 x => swap x j j_1) y (k :: l))[↑i] = y[↑i]