fact: Definition remove_impl : set A -> set A -> set A := fun E F x => E x /\ ~ F x.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)