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