bind 1 m1 : {v : Map_t Int Int | v = Map_default 0}
bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } 
bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 130 3) 110 1) 120 2) } 

constraint:
  env [ 1; 2; 3 ]
  lhs {v : Map_t Int Int | v = Map_shift 100 m2}
  rhs {v : Map_t Int Int | v = m3 } 
  id 1 tag []