proposition: Lemma eq_mem_mem : forall s e e', eq_A e e' -> mem e s -> mem e' s.
proof: Proof. intros s e e' e_eq_e' e_mem_s; destruct (mem_split_set _ _ eq_bool_ok _ _ e_mem_s) as [a [l' [l'' [e_eq_a [H _]]]]]. unfold mem; rewrite H. rewrite <- mem_or_app; right; left. transitivity e; trivial. symmetry; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)