include "utilities/Compare.ma".
include "utilities/BitVectorTrieSet.ma".
include "common/AST.ma".

axiom compare: Identifier → Identifier → Compare.
definition IdentifierSet ≝ BitVectorTrieSet 8.
axiom Universe: Type[0].
axiom fresh_prefix: IdentifierSet → Identifier → Identifier.
axiom new_universe: Identifier → Universe.
axiom fresh: Universe → Identifier.