proposition: Lemma rem_cardinal_lt: forall s x, StateSetSet.In x s -> StateSetSet.cardinal (StateSetSet.remove x s) < StateSetSet.cardinal s.
proof: Proof. intros. rewrite <- (StateSetSetProps.Props.remove_cardinal_1 H) ; auto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)