proposition: Lemma from_list_spec : forall x L, x \in from_list L = LibList.mem x L.
proof: Proof. Proof using. unfold from_list. induction L; rew_listx. rewrite in_empty. auto. rewrite in_union, in_singleton. congruence. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)