proposition: Lemma elements_Equal_eqlistA : forall (m m': t elt), Equal m m' -> eqlistA eqke (elements m) (elements m').
proof: Proof. intros. apply sort_equivlistA_eqlistA. 1-2: auto with map. red; intros. destruct x; do 2 rewrite <- elements_mapsto_iff. do 2 rewrite find_mapsto_iff; rewrite H; split; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface