Suggest an attempt to model Java arrays.

Example:

a = new T[10];
b = new T[10];

a = b;
i = j;

a[i] = 1;
b[j] = 2;
assert a[i]==1;

One possible model: arrays ::

What is desugaring of a[i]=x ?

array = array((a,i) := x);