intro hik hjk
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
⊢ ↑i ≠ k → ↑j ≠ k → (as.swap i j)[k] = as[k]
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]