proposition: Lemma disjoint_inj_rec (st : {set 'I_(size (to_word t))}) (s0 : {set 'I_(size t0)}) : [disjoint lsh_rec @: st & rsh_rec @: s0].
proof: Proof. Proof using. rewrite /lsh_rec /rsh_rec !imset_comp. rewrite -setI_eq0 -imsetI; last by move=> i j _ _ /= /cast_ord_inj. have := (disjoint_inj st s0); rewrite -setI_eq0 => /eqP ->. by rewrite imset0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype