proposition: Lemma extract1 i : extract [set i] = [:: tnth wt i].
proof: Proof. Proof using. rewrite /= extractIE. rewrite [filter _ _](_ : _ = [:: i]) //. rewrite (eq_filter (a2 := pred1 i)); last by move=> j /=; rewrite in_set1. apply: filter_pred1_uniq; first exact: enum_uniq. by rewrite mem_enum inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype