proposition: Lemma statesetset_map_in p: StateSetSet.In p (statesetset_map f t0) -> exists2 q, StateSetSet.In q t0 & StateSet.Equal (f q) p.
proof: Proof. unfold statesetset_map. apply StateSetSetProps.Props.fold_rec_nodep. StateSetSetProps.setdec. intros q a Hq IH. StateSetSetProps.Facts.set_iff. intros [Hp|Hp]; eauto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)