proposition: Lemma mask_uniq s : uniq s -> forall m, uniq (mask m s).
proof: Proof. elim: s => [|x s IHs] Uxs [|b m] //=. case: b Uxs => //= /andP[s'x Us]; rewrite {}IHs // andbT. by apply: contra s'x; apply: mem_mask. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)