if hij : i.1 = j then
  cases hij; simp only [get_set_eq]
else
  simp only [get_set_ne (h:=hij)]
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
a b : α
j : Nat
hj : j < n
⊢ (set (set x i a) i b)[j] = (set x i b)[j]
no goals