proposition: Lemma trivIseq_tabcols (t : seq (seq Alph)) : trivIseq (tabcols t).
proof: Proof. Proof using. apply: trivIseq_map; first by apply: cast_ord_inj. exact: trivIseq_shcols. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype