proposition: Lemma to_word_map_tab (t : seq (seq T1)) : to_word [seq map F r | r <- t] = map F (to_word t).
proof: Proof. by rewrite /to_word map_flatten map_rev. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted