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