proposition: Lemma already_mem_add : forall e s, mem e s -> add e s = s.
proof: Proof. intros a [l prf]; unfold mem, add; simpl; generalize (mem_bool_ok _ _ EDS1.eq_bool_ok a l). case (mem_bool EDS1.eq_bool a l). intros; reflexivity. intros a_not_in_l a_in_l; apply False_rect; apply a_not_in_l; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)