-- ********
--! FUNS
-- ********

-- ********
--! RULES
-- ********

equals_empty_nonempty b e =
  []
  |=
  emptybag `equals` (nonemptybag e b)
  <=>
  False

union_union_single b1 b2 e =
  []
  |=
  b1 `unionbag` singletonbag e `unionbag` b2
  <=>
  nonemptybag e (b1 `unionbag` b2)

-- ********
--! CLAUSES
-- ********