induction l with
| nil => intros; rfl
| cons k l IH =>
  intro y
  simp only [List.mem_cons, not_or] at h 
  specialize IH ⟨h.1,h.2.2⟩ y
  dsimp only [List.foldr]
  rewrite [get_swap, if_neg (Fin.val_ne_of_ne <| Ne.symm h.2.1), if_neg (Fin.val_ne_of_ne <| Ne.symm h.1)]
  exact IH
case cons
n : Nat
i j : Fin n
l : List (Fin n)
h : ¬i = j ∧ ¬i ∈ l
⊢ ∀ (y : Permutation n), (List.foldr (fun j_1 x => swap x j j_1) y l)[↑i] = y[↑i]
no goals