proposition: Lemma finite_tabsh : Finite.axiom tabsh_enum.
proof: Proof. Proof using. case=> /= t Ht; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)). rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first. by rewrite isSome_insub; case: eqP=> // ->. move: Ht => /andP[Htab /eqP Hsh]. rewrite count_map. have Htw : size (to_word t) == d. by rewrite size_to_word /size_tab Hsh sumn_intpartn. rewrite (eq_in_count (a2 := pred1 (Tuple Htw))). by rewrite enumT; apply: enumP (Tuple Htw). move=> w _ /=; apply/idP/idP. - move=> /eqP Ht; subst t. apply/eqP/val_inj => /=; rewrite /to_word revK. by apply esym; apply: reshapeKr; rewrite sumn_rev size_tuple sumn_intpartn. - move=> /eqP Hw; subst w; rewrite /=. by rewrite /to_word -Hsh -shape_rev flattenK revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted