proposition: Lemma msetU1l x A B : x \in A -> x \in A `|` B.
proof: Proof. by move=> Ax /=; rewrite inE Ax. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap