proposition: Lemma extractIE n (wt : n.-tuple Alph) P : extractpred wt P = [seq tnth wt i | i <- enum 'I_n & P i].
proof: Proof. Proof using. by rewrite /extractpred {1}/enum_mem -enumT /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype