cases Fin.eq_of_val_eq h
α : Type u
as : Array α
i j : Fin (size as)
h : i.val = j.val
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)
case refl
α : Type u
as : Array α
i : Fin (size as)
h : i.val = i.val
⊢ List.set (List.set as.data i.val (get as i)) i.val (get as i) =
    List.set (List.set as.data i.val (get as i)) i.val (get as i)