proposition: Lemma mclosure_sub s : s \subset mclosure s.
proof: Proof. apply/subsetP=> x; rewrite !inE => xIs. rewrite (_ : _ |: _ = s) //. by apply/setUidPr/subsetP=> y; rewrite inE => /eqP->. Qed.
imports: mathcomp(all_ssreflect)