fact: Definition add_classes t := fun i => StateSetSet.add (DS.class_of t (num_of_nat i)).
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)