proposition: Lemma add_12 : forall e e' s, mem e (add e' s) -> eq_A e e' \/ mem e s.
proof: Proof. intros e e' s; unfold mem, add; simpl; generalize (mem_bool_ok _ _ eq_bool_ok e' s.(support)). case (mem_bool eq_bool e' s.(support)). intros _ H; right; assumption. simpl; intros _ H; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)