proposition: Lemma size_cover_inj (T1 T2 : finType) (F : T1 -> T2) (P : {set {set T1}}): injective F -> #|cover P| = #|cover [set F @: S | S : {set T1} in P]|.
proof: Proof. move=> Hinj. set FSet := fun S : {set T1} => F @: S. suff -> : cover [set FSet S | S in P] = FSet (cover P) by rewrite card_imset. rewrite cover_imset /cover; apply: esym. by apply: big_morph; [exact: imsetU | exact: imset0]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype