proposition: Lemma extractmaskE n (wt : n.-tuple Alph) P : extractpred wt P = mask [seq P i | i <- enum 'I_n] wt.
proof: Proof. Proof using. rewrite extractIE. elim: n wt P => [// | n IHn]. - by rewrite enum0. - case/tupleP=> w0 w P; rewrite enum_ordSl /=. set lft := map (lift ord0) _. suff : [seq tnth [tuple of w0 :: w] i | i <- lft & P i] = mask [seq P i | i <- lft] w. by case: (P ord0) => /= ->. rewrite {}/lft filter_map -map_comp -map_comp /= -(IHn w _) /=. by rewrite (eq_map (g := tnth w)); last by move=> i /=; rewrite !(tnth_nth w0). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype