proposition: Lemma equal_mem_1: (forall a, mem a s=mem a s') -> equal s s'=true.
proof: Proof. intros; apply equal_1; unfold Equal; intros. do 2 rewrite mem_iff; rewrite H; tauto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx