proposition: Lemma is_yam_cat_any y0 y1 z : is_yam y0 -> is_yam y1 -> evalseq y0 = evalseq y1 -> is_yam (z ++ y0) -> is_yam (z ++ y1).
proof: Proof. elim: z => //= z0 z IHz Hy0 Hy1 H /andP[Hpart Hyam]. apply/andP; split; last exact: IHz. suff <- : evalseq (z ++ y0) = evalseq (z ++ y1) by []. apply /eqP; rewrite -perm_evalseq. by rewrite perm_cat2l perm_evalseq H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition