proposition: Lemma inter_1_aux : forall acc l1 l2 e, In e (remove_not_common acc l1 l2) -> In e acc \/ In e l1.
proof: Proof. intros acc l1 l2; generalize acc l1; clear acc l1; induction l2 as [ | e2 l2]. intros acc l1; simpl; intros; left; trivial. intros acc l1 e; simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]. intros H; destruct (IHl2 _ _ _ H) as [[ e2_eq_e | e_in_acc ] | e_in_l1 ]; clear H. subst; right; trivial. left; trivial. right; trivial. intros H; apply IHl2; trivial. Qed.
imports: List more_list list_permut Arith