proposition: Lemma of_list_2 : forall l, equivlistA E.eq (to_list (of_list l)) l.
proof: Proof. unfold to_list; red; intros. rewrite <- elements_iff; apply of_list_1. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide