intro k l hk hl has
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ ∀ (i_1 j_1 : Nat) (hi : i_1 < size (swap as i j)) (hj : j_1 < size (swap as i j)),
    (swap as i j)[i_1] = (swap as i j)[j_1] → i_1 = j_1
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ k = l