proposition: Lemma of_list_2 : forall l, NoDupA eqk l -> equivlistA eqke l (to_list (of_list l)).
proof: Proof. intros l Hnodup (k,e). rewrite <- elements_mapsto_iff, of_list_1; intuition. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface