fact: Structure cmpType := mk_cmp { carr:> Set; eqb: carr -> carr -> bool; _: forall x y, reflect (x=y) (eqb x y); cmp: carr -> carr -> comparison; _: forall x y, compare_spec (x=y) (cmp x y) }.
imports: List Eqdep Eqdep_dec