proposition: Lemma measure_empty: forall size, measure size DS.empty = size.
proof: Proof. unfold measure. induction size as [|s IHs]. reflexivity. simpl. rewrite add_classes_empty. rewrite StateSetSetProps.Props.add_cardinal_2. rewrite IHs. reflexivity. clear IHs. induction s; simpl. StateSetSetProps.setdec. rewrite add_classes_empty. StateSetSetProps.set_iff. clear. intros [H|H]. eapply proj1 in H. apply apply in H. 2: rewrite StateSetProps.singleton_iff; trivial. revert H. StateSetProps.set_iff. intro. psubst. revert H. generalize (statesetelt_of_nat s). intro. num_lia. apply in_classes_empty_below in H. specialize (H (Pos.succ (state_of_nat s))). apply apply in H. num_lia. auto with set. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)