dsimp only [List.foldr]
case cons.cons
n : Nat
i j k : Fin n
l : List (Fin n)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (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)
y : Permutation n
h : ¬i = j ∧ ¬i = k ∧ ¬i ∈ l
IH : (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
⊢ (swap (List.foldr (fun j_1 x => swap x j j_1) y l) j k)[↑i] = y[↑i]