bind 1 b1 : {v : Bag_t Int | v = Bag_empty 0 }
bind 2 b2 : {v : Bag_t Int | v = (Bag_union (Bag_sng 10 1) (Bag_sng 20 1)) }
bind 3 b3 : {v : Bag_t Int | v = (Bag_union (Bag_sng 20 1) (Bag_sng 10 1)) }
bind 4 b4 : {v : Bag_t Int | v = (Bag_sng 10 1) }
bind 5 b5 : {v : Bag_t Int | v = (Bag_sng 20 1) }

constraint:
  env [ 1 ]
  lhs {v : int | v = Bag_count 100 b1 }
  rhs {v : int | v = 0 }
  id 1 tag []

constraint:
  env [ 2 ]
  lhs {v : int | v = Bag_count 100 b2 }
  rhs {v : int | v = 0 }
  id 2 tag []

constraint:
  env [ 2 ]
  lhs {v : int | v = Bag_count 10 b2 }
  rhs {v : int | v = 1 }
  id 3 tag []

constraint:
  env [ 2; 3 ]
  lhs {v : int | true }
  rhs {v : int | b2 = b3 }
  id 4 tag []

constraint:
  env [ 2; 4; 5 ]
  lhs {v : int | true }
  rhs {v : int | b2 = Bag_union b4 b5 }
  id 5 tag []

constraint:
  env [ 2; 4 ]
  lhs {v : bool | v = Bag_sub b4 b2 }
  rhs {v : bool | v = true }
  id 6 tag []

constraint:
  env [ 3; 5 ]
  lhs {v : bool | v = Bag_sub b3 b5 }
  rhs {v : bool | v = false }
  id 7 tag []