intros
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y [])[↑i] = y[↑i]
case cons.nil
n : Nat
i j : Fin n
h : ¬i = j ∧ ¬i ∈ []
y✝ : Permutation n
⊢ (List.foldr (fun j_1 x => swap x j j_1) y✝ [])[↑i] = y✝[↑i]