simp [Vec.swap_def]
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ (a.swap i j)[k] = a[k]
α : Type
n : Nat
a : Vec α n
i j k : Fin n
ki : k ≠ i
kj : k ≠ j
⊢ ((a.set i (a.get j)).set j (a.get i))[k] = a[k]