proposition: Lemma set_in_inter_eq : forall x E F, x \in (E \n F) = (x \in E /\ x \in F).
proof: Proof. Proof using. apply in_inter_eq. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)