proposition: Lemma inter_2_aux : forall acc l1 l2 e, more_list.mem eq_A e (remove_not_common acc l1 l2) -> more_list.mem eq_A e acc \/ more_list.mem eq_A e l2.
proof: Proof. intros acc l1 l2 e e_in_acc_l2; functional induction (remove_not_common acc l1 l2) as [ | acc l1 H1 e2 l2 H2 e2_in_l1 IH | acc l1 H1 e2 l2 H2 e2_not_in_l1 IH]. left; trivial. destruct (IH e_in_acc_l2) as [[e_eq_e2 | e_in_acc] | e_in_l1]; [ subst; right; left | left | right; right ]; trivial. destruct (IH e_in_acc_l2) as [e_in_acc | e_in_l2]; [left | right; right]; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)