proposition: Lemma in_intersect : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A) a, In a (intersect eqd ls1 ls2) <-> In a ls1 /\ In a ls2.
proof: Proof. unfold intersect in *. intuition. apply filter_In in H. intuition. destruct (in_dec eqd a ls1). trivial. discriminate. apply filter_In in H. intuition. eapply filter_In. intuition. destruct (in_dec eqd a ls1); intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia