fact: Definition domain t := StateSetMap.fold (fun p (np: T) a => StateSetSet.add p a) t StateSetSet.empty.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)