theory Test_simplify_array
  use import array.Array
  goal G1 : forall x y:int. forall m: t int int.
    get (set m y x) y = x
  goal G2 : forall x y y' z t:int. forall m: t int int.
    z <> x ->
    get m z = y ->
    get (set m x t) z = y
  goal G3 : forall y t:int. forall m: t int int.
    get m 1 = y ->
    get (set m 2 t) 1 = y
  goal G4 : forall x y:int. forall m: t int int.
    get (set (set m 2 y) 1 x) 2 = y
end