proposition: Lemma is_empty_equal_empty: is_empty s = equal s empty.
proof: Proof. apply bool_1; split; intros. - auto with set. - rewrite <- is_empty_iff; auto with set. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx