proposition: Lemma inter_add_2: mem x s'=false -> equal (inter (add x s) s') (inter s s')=true.
proof: Proof. intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx