proposition: Lemma add_1 : forall e s, mem e (add e s).
proof: Proof. intros e s; unfold mem, add; simpl. generalize (mem_bool_ok _ _ eq_bool_ok e s.(support)). case (mem_bool eq_bool e s.(support)). intro H; exact H. simpl; intros _; left; reflexivity. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)