proposition: Lemma measure_compat: forall size `{DS.WF} {t'} `{DS.WF t'}, t [=T=] t' -> measure size t = measure size t'.
proof: Proof. intros. apply StateSetSetProps.Props.Equal_cardinal, classes_compat; trivial. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)