proposition: Lemma union_2_aux : forall (l1 l2 : list A) (e : A), more_list.mem eq_A e l2 -> more_list.mem eq_A e (add_without_red l1 l2).
proof: Proof. fix union_2_aux 2. intros l1 l2; case l2; clear l2. intros; contradiction. intros a2 l2 e e_in_a2l2; simpl in e_in_a2l2; simpl. case e_in_a2l2; clear e_in_a2l2. intro e_eq_a2. refine (mem_eq_mem eq_proof a2 e _ (equiv_sym _ _ eq_proof _ _ e_eq_a2) _); simpl. generalize (mem_bool_ok _ _ eq_bool_ok a2 l1); case (mem_bool eq_bool a2 l1). intro a2_in_l1; apply union_1_aux; assumption. intros _; apply (union_1_aux (a2 :: l1) l2); left; reflexivity. intro e_in_l2; case (mem_bool eq_bool a2 l1); apply union_2_aux; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)