proposition: Lemma in_mask x m s : uniq s -> x \in mask m s = (x \in s) && nth false m (index x s).
proof: Proof. elim: s m => [|y s IHs] [|[] m]//= /andP[yNs ?]; rewrite ?in_cons ?IHs //=; by have [->|neq_xy] //= := eqVneq; rewrite ?andbF // (negPf yNs). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)