intro k hk hk'
α : Type u
x : Array α
i j : Fin (size x)
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < size (swap x i j)) (hi₂ : i_1 < size (swap x j i)), (swap x i j)[i_1] = (swap x j i)[i_1]
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (swap x i j)[k] = (swap x j i)[k]