proposition: Lemma union_1_aux : forall (l1 l2 : list A) (e : A), more_list.mem eq_A e l1 -> more_list.mem eq_A e (add_without_red l1 l2).
proof: Proof. fix union_1_aux 2. intros l1 l2; case l2; clear l2. intros; assumption. intros a2 l2 e e_in_l1; simpl. case (mem_bool eq_bool a2 l1). apply (union_1_aux l1 l2 _ e_in_l1). apply (union_1_aux (a2 :: l1) l2 _ (or_intror _ e_in_l1)). Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)