proposition: Lemma compat_negsplit s: compat_bool StateSet.Equal (fun p => negb (StateSet.mem s p)).
proof: Proof. intros ? ? H. rewrite H. trivial. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)