proposition: Lemma mask_injP : reflect (injective (fun m : (size w).-tuple bool => mask (val m) w)) (uniq w).
proof: Proof. apply (iffP idP) => [w_uniq m1 m2 eqmask |]. - apply: eq_from_tnth => i; rewrite !(tnth_nth false). have Z : T by case: w i {w_uniq m1 m2 eqmask} => [[]|]. have nthE m : (nth false m i) = (nth Z w i \in mask m w). by rewrite in_mask // (mem_nth Z (ltn_ord i)) /= index_uniq. by rewrite !nthE eqmask. - case Hw: w => [// |w0 w']; rewrite -Hw => minj. pose f := (fun i : T => [:: i]). apply/(uniqP w0) => i j; rewrite !inE => lti ltj Heq. move/(congr1 (cons^~ [::]) (x := _) (y := _)): Heq. rewrite -!mask1E // => /minj /(congr1 (fun t => tnth t (Ordinal lti))). by rewrite !tnth_mktuple /= eqxx => /esym/eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted