proposition: Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s.
proof: Proof. intros s k. rewrite of_list_1b, elements_o; auto. apply elements_3w. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface