proposition: Lemma intersect_comm : 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. apply filter_NoDup; trivial. apply filter_NoDup; trivial. unfold intersect in *. intuition. apply filter_In. apply filter_In in H1. intuition. destruct (in_dec eqd x ls1); intuition. discriminate. destruct (in_dec eqd x ls2); intuition. apply filter_In. apply filter_In in H1. intuition. destruct (in_dec eqd x ls2); intuition. discriminate. destruct (in_dec eqd x ls1); intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia