proposition: Lemma mask_filter s m : uniq s -> mask m s = [seq i <- s | i \in mask m s].
proof: Proof. elim: m s => [|[] m IH] [|x s /= /andP[/negP xS uS]]; rewrite ?filter_pred0 //. rewrite inE eqxx /=; congr cons; rewrite [LHS]IH//. by apply/eq_in_filter => ? /[1!inE]; case: eqP => [->|]. by case: ifP => [/mem_mask //|_]; apply: IH. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)