Improve the extraction of code manipulating arrays/slices

[sonmarcho]

When extracting Rust code of the following shape:

a[i] = x + y;

We get:

let (_, index_mut_back) ← Array.index_mut_usize a i
let tmp ← x + y
let a1 := index_mut_back tmp

We want to get:

let tmp ← x + y
let a1 ← update a i tmp

We can easily do so through a micro-pass (there already exists one for array/slice indexing functions: we simply need to improve it).

[R1kM]

Similar to https://github.com/AeneasVerif/aeneas/issues/188

[sonmarcho]

Ah indeed. But I'm closing this other issue because I took care of it in a recent PR. I basically need to generalize the micro-pass I implemented for it.