proposition: Lemma add_classes_empty: forall x a, StateSetSet.Equal (add_classes DS.empty x a) (StateSetSet.add (StateSet.singleton x) a).
proof: Proof. intros. unfold add_classes. rewrite DSUtils.class_of_empty. reflexivity. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)