proposition: Lemma msets_sub s1 s2 : s1 \subset s2 -> s2 \in msets M -> s1 \in msets M.
proof: Proof. move=> s1Ss2 s2IM. have /and3P[_ /forallP/(_ s1)/forallP/(_ s2) H _] := wf_msets M. by have /implyP->// := H; rewrite s1Ss2. Qed.
imports: mathcomp(all_ssreflect)