proposition: Lemma union_12_aux : forall (l1 l2 : list A) (e : A), more_list.mem eq_A e (add_without_red l1 l2) -> more_list.mem eq_A e l1 \/ more_list.mem eq_A e l2.
proof: Proof. intros l1 l2 e e_in_l1_l2; functional induction (add_without_red l1 l2) as [ | l1 H1 e2 l2 H2 e2_in_l1 IH | l1 H1 e2 l2 H2 e2_not_in_l1 IH ]. left; trivial. destruct (IH e_in_l1_l2) as [e_in_l1 | e_in_l2]; [left | do 2 right]; trivial. destruct (IH e_in_l1_l2) as [[e_eq_e2 | e_in_l1] | e_in_l2]; [ right; left | left | do 2 right]; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)