Firstly, you can define a ghost sequence which clones the array. You can then write two-state lemmas about the array. I happened to write a blog post about a very similar situation here.

https://dev.to/hath995/verified-ordered-set-in-dafny-2aak