rfl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.set
      (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
        (Array.get x.val (Fin.cast (_ : n = Array.size x.val) j)))
      { val := ↑(Fin.cast (_ : n = Array.size x.val) j),
        isLt :=
          (_ :
            ↑(Fin.cast (_ : n = Array.size x.val) j) <
              Array.size
                (Array.set x.val (Fin.cast (_ : n = Array.size x.val) i)
                  x.val[↑(Fin.cast (_ : n = Array.size x.val) j)])) }
      (Array.get x.val (Fin.cast (_ : n = Array.size x.val) i)) =
    (set (set x i x[↑j]) j x[↑i]).val
no goals