proposition: Lemma union_12_aux : forall (l1 l2 : list elt) (e : elt), In e (add_without_red l1 l2) -> In e l1 \/ In e l2.
proof: Proof. intros l1 l2; generalize l1; clear l1; induction l2 as [ | e2 l2]; intros l1 e; simpl. intro; left; trivial. destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. intro H; generalize (IHl2 _ _ H); intuition. intro H; generalize (IHl2 _ _ H); simpl; intuition. Qed.
imports: List more_list list_permut Arith