proposition: Lemma without_red_remove_not_common_aux : forall acc l1 l2, (forall e, more_list.mem eq_A e acc /\ more_list.mem eq_A e l2 -> False) -> without_red acc -> without_red l1 -> without_red l2 -> without_red (remove_not_common acc l1 l2).
proof: Proof. intros acc l1 l2 H Wa Wl1 Wl2; functional induction (remove_not_common acc l1 l2) as [ | acc l1 H1 e l2 H2 e_in_l1 IH | acc l1 H1 e l2 H2 e_not_in_l1 IH]. trivial. apply IH. simpl; intros a H'; case H'; clear H'; intro H'; case H'; clear H'. intros a_eq_e; revert Wl2; unfold without_red; simpl. generalize (mem_bool_ok _ _ eq_bool_ok e l2); case (mem_bool eq_bool e l2). intros _ Abs _; discriminate. intros e_not_in_l2 _ e_in_l2; apply e_not_in_l2. apply (mem_eq_mem eq_proof a); assumption. intros a_in_acc a_in_l2; apply (H a); split; [idtac | right]; assumption. unfold without_red; simpl. generalize (mem_bool_ok _ _ eq_bool_ok e acc); case (mem_bool eq_bool e acc). intro e_in_acc; apply False_rect; apply (H e); split; [assumption | left; reflexivity]. intros _; unfold without_red in Wa; assumption. assumption. revert Wl2; unfold without_red; simpl; case (mem_bool eq_bool e l2). intro; discriminate. intro; assumption. apply IH. simpl; intros a H'; case H'; clear H'. intros a_in_acc a_in_l2; apply (H a); split; [idtac | right]; assumption. assumption. assumption. revert Wl2; unfold without_red; simpl; case (mem_bool eq_bool e l2). intro; discriminate. intro; assumption. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)