proposition: Lemma mem_consn : forall a ll, mem EDS.eq_A a (consn ll) <-> exists la, In (a,la) ll.
proof: Proof. intros a ll; split; intro H; functional induction (consn ll) as [ | H1 b lb ll H2 IH]. contradiction. simpl in H; destruct H as [a_eq_b | a_in_cnsl]. dummy a b a_eq_b; exists lb; subst; left; trivial. destruct (IH a_in_cnsl) as [la H]. exists la; right; trivial. destruct H; contradiction. destruct H as [la [ala_eq_blb | ala_in_ll]]. injection ala_eq_blb; intros; subst; left; apply (equiv_refl _ _ eq_proof); trivial. right; apply IH; exists la; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)