proposition: Lemma subset_mem_1: (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
proof: Proof. intros; apply subset_1; unfold Subset; intros a. do 2 rewrite mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx