proposition: Lemma trivIseq_map (T1 T2 : finType) (f : T1 -> T2) (S : seq {set T1}) : injective f -> trivIseq S -> trivIseq (map (fun s : {set T1} => f @: s) S).
proof: Proof. move=> Hinj; rewrite /trivIseq => H i j /andP[]. rewrite size_map => Hij Hj; have Hi := ltn_trans Hij Hj. rewrite /disjoint; apply/pred0P => l /=; apply/negP => /andP[]. rewrite !(nth_map set0) //=. move/imsetP => [li Hli -> {l}] /imsetP[l Hlj /Hinj Heq]; subst li. have : i < j < size S by rewrite Hij Hj. by move/(H i j); rewrite /disjoint => /pred0P/(_ l); rewrite /= Hli Hlj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast