simp [Vec.swap]
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ a.swap i j = (a.set i (a.get j)).set j (a.get i)
α : Type
n : Nat
a : Vec α n
i j : Fin n
⊢ ⟨a.val.swap (Fin.cast ⋯ i) (Fin.cast ⋯ j), ⋯⟩ = (a.set i (a.get j)).set j (a.get i)