proposition: Lemma S1_subsST : S1 \subset (S :|: T).
proof: Proof. Proof using. by apply/subsetP=> i; rewrite !inE => /orP[] /andP[-> _]; last rewrite orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene