cases q <;> simp [Id.run]
α : Type u_1
arr : Array α
f : α → α
n : Nat
q : Decidable (n < size arr)
⊢ size arr = size (Id.run (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) q))
no goals