proposition: Lemma plact_uniq_revE u v : uniq u -> (u =Pl v) = (rev u =Pl rev v).
proof: Proof. Proof using. move=> Hu; apply/idP/idP; first exact: plact_uniq_rev. rewrite -{2}(revK u) -{2}(revK v). by apply: plact_uniq_rev; rewrite rev_uniq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr