proposition: Lemma to_list_empty : to_list (\{}:set A) = nil.
proof: Proof. Proof using. set_unf. epsilon l. { exists (@nil A). split. { constructor. } { intros. rewrite* mem_nil_eq. } } intros Hl. inverts Hl. simpls. destruct~ l. false. rewrite <- H0. simple~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)