proposition: Lemma size_bound (x : word) (s : seq word) : all (szinvar x) s -> uniq s -> size s <= #|Alph|^(size x).
proof: Proof. Proof using. pose T := (size x).-tuple Alph. rewrite -card_tuple cardE all_count => /eqP Hall /(pmap_sub_uniq T). have := size_pmap_sub T s; rewrite Hall => <-. by apply: (full_bound _ (all_predT _)) => u _; rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK