Set Implicit Arguments.

Require Import Arith.
Require Import MultisetTheory.
Require Import MultisetOrder.
Require Import MultisetList.
Require Import RelExtras.

Module Nat.
  Definition A := nat.
End Nat.

Module NatSet <: Eqset := Eqset_def Nat.

Module NatSet_dec.

  Module Eq := NatSet.
  Export Eq.

  Definition eqA_dec := eq_nat_dec.

End NatSet_dec.

Module MSetCore := MultisetList.MultisetList NatSet_dec.

Module MSetTheory := MultisetTheory.Multiset MSetCore.
Notation "'XXX'" := I : sets_scope.
Export MSetTheory.

Module MSetOrd := MultisetOrder.MultisetOrder MSetCore.
Export MSetOrd.