proposition: Lemma intersect_comm_Permutation : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A), NoDup ls1 -> NoDup ls2 -> Permutation (intersect eqd ls1 ls2) (intersect eqd ls2 ls1).
proof: Proof. intuition. eapply NoDup_Permutation; intuition. eapply intersect_NoDup. trivial. eapply intersect_NoDup. trivial. unfold intersect in *. apply filter_In in H1. intuition. eapply filter_In; intuition. destruct (in_dec eqd x ls1); try congruence. destruct (in_dec eqd x ls2); intuition. unfold intersect in *. apply filter_In in H1. intuition. eapply filter_In; intuition. destruct (in_dec eqd x ls2); try congruence. destruct (in_dec eqd x ls1); intuition. Qed.
imports: FCF.FCF Permutation