proposition: Lemma eqb_of_compare_spec A f: (forall a b: A, compare_spec (a=b) (f a b)) -> forall a b, reflect (a=b) (eqb_of_compare f a b).
proof: Proof. unfold eqb_of_compare. intros H a b. now case H; constructor. Qed.
imports: List Eqdep Eqdep_dec