proposition: Lemma of_list_3 : forall s, of_list (to_list s) [=] s.
proof: Proof. unfold to_list; red; intros. rewrite of_list_1; symmetry; apply elements_iff. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide