proposition: Lemma inter_1_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 l1.
proof: Proof. intros acc l1 l2 e e_in_acc_l1; 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_l1) as [[e_eq_e2 | e_in_acc] | e_in_l1]; [ subst; right | left | right ]; trivial. apply (mem_eq_mem eq_proof e2). apply (equiv_sym _ _ eq_proof); assumption. generalize (mem_bool_ok _ _ eq_bool_ok e2 l1); rewrite e2_in_l1; intro H; exact H. apply IH; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)