theory ModelArray

use map.Map

goal t1 : forall t: map int int, i: int.
   get (set t 0 42) i = get t i

end