open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Identifiers

type costlabel = PreIdentifiers.identifier

(** val costlabel_eq : costlabel -> costlabel -> (__, __) Types.sum **)
let costlabel_eq =
  Identifiers.identifier_eq PreIdentifiers.CostTag

(** val costlabel_of_nat : Nat.nat -> costlabel **)
let costlabel_of_nat =
  Identifiers.identifier_of_nat PreIdentifiers.CostTag