proposition: Lemma Equal_Equivb_eqdec : forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }), let cmp := fun e e' => if eq_elt_dec e e' then true else false in forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.
proof: Proof. intros; apply Equal_Equivb. unfold cmp; clear cmp; intros. destruct eq_elt_dec; now intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface