proposition: Lemma set_nil (T : finType) : [set s : T in [::]] = set0.
proof: Proof. by apply/setP => i; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast