proposition: Lemma union_2_aux : forall (l1 l2 : list elt) (e : elt), In e l2 -> In e (add_without_red l1 l2).
proof: Proof. intros l1 l2; generalize l1; clear l1; induction l2 as [ | e2 l2]; intros l1 e e_in_e2l2. contradiction. simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1]; destruct e_in_e2l2 as [e_eq_e2 | e_in_l2]. subst; apply union_1_aux; trivial. apply IHl2; trivial. subst; apply union_1_aux; left; trivial. apply IHl2; trivial. Qed.
imports: List more_list list_permut Arith