proposition: Lemma cast_enum u (S : {set 'I_(size u)}) : enum (mem (cast_set (esym (size_std u)) S)) = map (cast_ord (esym (size_std u))) (enum (mem S)).
proof: Proof. Proof using. rewrite {1}/enum_mem -enumT /=. rewrite -[filter _ _]map_id (cast_map_cond _ _ (esym (size_std u))). congr (map _ _). rewrite {2}/enum_mem -enumT /=. apply: eq_filter => i /=. exact/mem_imset/cast_ord_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv