proposition: Lemma to_word_enum_tabsh : perm_eq [seq to_word (tabshval t) | t : tabsh] [seq x <- [seq (i : seq _) | i : d.-tuple T] | tabsh_reading sh x].
proof: Proof. Proof using. apply uniq_perm. - rewrite map_inj_in_uniq; first exact: enum_uniq. move=> t u _ _ /= Heq; apply val_inj. by rewrite /= -(tabsh_to_wordK t) -(tabsh_to_wordK u) Heq /=. - apply filter_uniq; rewrite map_inj_uniq; last exact: val_inj. exact: enum_uniq. move=> w /=; rewrite /tabsh_reading mem_filter; apply/idP/idP. - move=> /mapP[t _ ->{w}]. rewrite size_to_word /size_tab shape_tabsh eq_refl /=. rewrite tabsh_to_wordK tabshP /=. have Ht : size (to_word (val t)) == d. by rewrite size_to_word /size_tab shape_tabsh sumn_intpartn. have -> : to_word (val t) = val (Tuple Ht) by []. rewrite mem_map; last exact: val_inj. exact: mem_enum. - move=> /andP[/andP[/eqP Hsz Htab] /mapP[tpl _ hw]]; subst w. have Htsh : is_tab_of_shape sh (rev (reshape (rev sh) tpl)). rewrite /is_tab_of_shape /= Htab /= shape_rev reshapeKl ?revK //. by rewrite sumn_rev Hsz. suff -> : val tpl = to_word (TabSh Htsh). by apply/mapP; exists (TabSh Htsh) => //; apply: mem_enum. rewrite /= /to_word revK reshapeKr //. by rewrite sumn_rev Hsz. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted