cases hjk
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ b = a
case t.t.refl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
hk : ↑j < n
hik : ↑i = ↑j
⊢ b = a