proposition: Lemma classes_compat: forall size `{DS.WF} {t'} `{DS.WF t'}, t [=T=] t' -> StateSetSet.Equal (classes size t) (classes size t').
proof: Proof. induction size as [|s IHs]; intros t t' H H'' Ht; simpl. reflexivity. apply StateSetSetProps.add_m; trivial. apply DSUtils.class_of_compat'; ti_auto. apply IHs; trivial. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)