proposition: Lemma measure_union_strict: forall `{DS.WF} size t' (x y: state), x < size -> y < size -> DS.equiv t x y = (false,t') -> measure size (DS.union t x y) < measure size t.
proof: Proof. intros. unfold measure. rewrite classes_union_strict; try eassumption. apply add_cardinal. rewrite StateSetSetProps.Props.remove_cardinal_1. apply rem_cardinal_lt. rewrite in_classes. exists y; trivial. bool_simpl; reflexivity. apply StateSetSet.remove_2. intro F. apply DSUtils.class_of_injective in F; trivial. apply (@Equivalence_Symmetric _ _ (@DS.sameclass_Equivalence _ H)) in F. rewrite <- DS.sameclass_equiv, H2 in F; trivial. discriminate. rewrite in_classes. exists x; trivial. bool_simpl; reflexivity. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)