proposition: Lemma mask1E x0 i : i < size w -> mask [tuple val x == i | x < size w] w = [:: nth x0 w i].
proof: Proof. move=> lti. rewrite [val (mktuple _)](_ : _ = [seq x == i | x <- iota 0 (size w)]); last by rewrite /= (map_comp (pred1 i) val) val_enum_ord. elim: w i lti => //= v0 v IHv [_|i /ltnSE lti] /=. rewrite [map _ _](_ : _ = nseq (size v) false) ?mask_false //. apply (eq_from_nth (x0 := false)) => [|i]. by rewrite size_map size_iota size_nseq. rewrite size_map => lti; rewrite (nth_map 0) //. by rewrite size_iota in lti; rewrite nth_nseq lti nth_iota. by rewrite -(add1n 0) iotaDl -map_comp -{}IHv. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted