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 10 1) 20 1) 30 1) } 

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

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

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

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

constraint:
  env [ 1; 2; 3 ]
  lhs {v : Map_t Int Int | v = Map_union_min m1 m2}
  rhs {v : Map_t Int Int | v = m1 } 
  id 5 tag []

constraint:
  env [ 1; 2; 3 ]
  lhs {v : Map_t Int Int | v = Map_union_min m1 m3}
  rhs {v : Map_t Int Int | v = m1 } 
  id 6 tag []