cases h
case mpr.mk.mk
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi : i < Array.size x.val
j : Nat
hj : j < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := j, isLt := hj }]
h : { val := i, isLt := (_ : i < n) } = { val := j, isLt := (_ : j < n) }
⊢ { val := i, isLt := hi } = { val := j, isLt := hj }
case mpr.mk.mk.refl
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
i : Nat
hi hj : i < Array.size x.val
hxij : x.val[↑{ val := i, isLt := hi }] = x.val[↑{ val := i, isLt := hj }]
⊢ { val := i, isLt := hi } = { val := i, isLt := hj }