Library set_instance
Defines a (trivial) decidable equality on
label
and
id
.
Require
Export
prog
.
Require
Export
set
.
Instance
DS_label
:
DecidableType
label
.
Proof
.
split
.
apply
Nat.eq_dec
.
Defined
.
Instance
DS_id
:
DecidableType
id
.
Proof
.
split
.
apply
eq_id_dec
.
Defined
.