proposition: Lemma union_subset_3: subset s s''=true -> subset s' s''=true -> subset (union s s') s''=true.
proof: Proof. intros; apply subset_1; apply union_subset_3; auto with set. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx