cases size_modifyM (m:=Id) x n f with | intro w hw =>
dsimp at hw
conv at hw => rhs; change modify x n f
rw [←hw]
exact w.property
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
⊢ size (modify x n f) = size x
no goals