no goals
α : Type ?u.19284
a : Array α
i : Fin (size a)
v v' : α
⊢ i.val < size (set a i v)
simp [i.2]
no goals
α : Type u_1
a : Array α
i : Fin (size a)
v v' : α
⊢ set (set a i v) { val := i.val, isLt := (_ : i.val < size (set a i v)) } v' = set a i v'
simp [set, List.set_set]