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