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