proposition: Lemma without_red_remove_not_common_aux : forall acc l1 l2, (forall e, In e acc /\ In 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; generalize acc l1; clear acc l1; induction l2 as [ | e2 l2]. intros; trivial. intros acc l1 H wra wr1 wr2; simpl; destruct (In_dec eq_elt_dec e2 l1) as [ e2_in_l1 | e2_not_in_l1 ]; apply IHl2; trivial. intros e [[e_eq_e2 | e_in_acc] e_in_l2]. subst e; simpl in wr2; destruct (In_dec eq_elt_dec e2 l2) as [ _ | e2_not_in_l2]; trivial; absurd (In e2 l2); trivial. apply (H e); split; trivial; right; trivial. simpl; destruct (In_dec eq_elt_dec e2 acc) as [ e2_in_acc | _]; trivial. apply (H e2); split; trivial; left; trivial. apply (without_red_remove e2 nil l2); trivial. intros e [e_in_acc e_in_l2]; apply (H e); split; trivial; right; trivial. apply (without_red_remove e2 nil l2); trivial. Qed.
imports: List more_list list_permut Arith