fact: Definition disjoint_impl : set A -> set A -> Prop := fun E F : set A => inter_impl E F = empty_impl.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)