proposition: Lemma union_1_aux : forall (l1 l2 : list elt) (e : elt), In e l1 -> In e (add_without_red l1 l2).
proof: Proof. intros l1 l2; generalize l1; clear l1; induction l2 as [ | e2 l2]. intros; trivial. intros l1 e e_in_l1; simpl; case ( In_dec eq_elt_dec e2 l1); intro; apply IHl2; trivial. right; trivial. Qed.
imports: List more_list list_permut Arith