proposition: Lemma in_appendn : forall a ll, mem EDS.eq_A a (appendn ll) -> exists b, exists lb, In (b,lb) ll /\ mem EDS.eq_A a lb.
proof: Proof. intros a ll H; functional induction (appendn ll) as [ | H1 b lb ll H2 IH]. contradiction. rewrite <- mem_or_app in H; destruct H as [a_mem_lb | a_mem_appl]. exists b; exists lb; split; trivial; left; trivial. destruct (IH a_mem_appl) as [c [lc [H1 H2]]]; exists c; exists lc; split; trivial; right; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)