proposition: Lemma to_list_single : forall (x:A), to_list (\{x}) = x::nil.
proof: Proof. Proof using. intros. unfold to_list. epsilon l. { exists (x::nil). split. { applys noduplicates_one. } { unfold single_inst, single_impl. simple~. intros. rewrite* mem_one_eq. } } introv Hl. unfolds single_inst, single_impl. simpls~. inverts Hl as H H0. destruct (H0 x). specializes~ H2. destruct l. { inverts H2. } { tests E: (x = a). { fequals. destruct l. auto. forwards~: (proj1 (H0 a0)). subst. inverts H as M1 M2. false* M1. } { inverts H2. false. forwards~: (proj1 (H0 a)). false. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)