proposition: Lemma measure_union_idem: forall `{DS.WF} size x y, {{t}} x y -> measure size (DS.union t x y) = measure size t.
proof: Proof. intros. eapply measure_compat; ti_auto. symmetry. apply DSUtils.eq_union; auto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)