proposition: Lemma Equal_Equivb : forall cmp, (forall e e', cmp e e' = true <-> e = e') -> forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.
proof: Proof. intros; rewrite Equal_Equiv. apply Equiv_Equivb; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface