proposition: Lemma domain_spec: forall x t, StateSetSet.In x (domain t) <-> StateSetMap.In x t.
proof: Proof. intros x t. unfold domain. refine (StateSetMapProps.fold_rec_bis (P:=fun m a => StateSetSet.In x a <-> StateSetMap.In x m) _ _ _). intros. rewrite <- H. assumption. StateSetSetProps.set_iff. StateSetMapProps.map_iff. tauto. intros. StateSetSetProps.set_iff. StateSetMapProps.map_iff. tauto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)