rewrite [getElem_swap]
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (swap x { val := i, isLt := hi } { val := j, isLt := hj })[↑{ val := i, isLt := hi }] = x[↑{ val := j, isLt := hj }]
case mk.mk
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
⊢ (if ↑{ val := j, isLt := hj } = ↑{ val := i, isLt := hi } then x[↑{ val := i, isLt := hi }]
    else
      if ↑{ val := i, isLt := hi } = ↑{ val := i, isLt := hi } then x[↑{ val := j, isLt := hj }]
      else x[↑{ val := i, isLt := hi }]) =
    x[↑{ val := j, isLt := hj }]