proposition: Lemma inter_12_aux : forall acc l1 l2 e, more_list.mem eq_A e l1 -> more_list.mem eq_A e l2 -> more_list.mem eq_A e (remove_not_common acc l1 l2).
proof: Proof. assert (H : forall acc l1 l2 e, more_list.mem eq_A e acc -> more_list.mem eq_A e (remove_not_common acc l1 l2)). intros acc l1 l2 e e_in_acc; 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]. trivial. apply IH; right; trivial. apply IH; trivial. intros acc l1 l2 e e_in_l1 e_in_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]. contradiction. destruct e_in_l2 as [e_eq_e2 | e_in_l2]; [subst; apply H; left | apply IH]; trivial. destruct e_in_l2 as [e_eq_e2 | e_in_l2]. absurd (more_list.mem eq_A e2 l1). generalize (mem_bool_ok _ _ eq_bool_ok e2 l1); rewrite e2_not_in_l1; intro H'; exact H'. apply (mem_eq_mem eq_proof e); assumption. apply IH; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)