cases hji
α : Type u
x : Subarray α
i : Nat
hi : i < size x
j : Nat
hj : j < size x
hji : j = i
⊢ (if j = i then x[i] else if i = i then x[j] else x[i]) = x[j]
case refl
α : Type u
x : Subarray α
i : Nat
hi hj : i < size x
⊢ (if i = i then x[i] else if i = i then x[i] else x[i]) = x[i]