proposition: Lemma in_classes: forall t size x, StateSetSet.In x (classes size t) <-> exists2 y, y<size & StateSet.Equal x (DS.class_of t (state_of_nat y)).
proof: Proof. induction size; intros x; simpl; unfold add_classes; StateSetSetProps.set_iff. intuition. destruct H. lia. rewrite IHsize. clear IHsize. completer idtac. symmetry in H. eauto with lia. destruct H. eauto with lia. destruct H as [y Hy H]. destruct (eq_nat_dec y size). subst. symmetry in H. auto. right. exists y. lia. assumption. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)