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.