proposition: Lemma evalseq_hyper_yam ev : is_part ev -> evalseq (hyper_yam ev) = ev.
proof: Proof. rewrite /hyper_yam; elim/last_ind: ev => // s sn IHs. rewrite rev_rcons /=; case: sn => [/= | sn]. by move/is_partP; rewrite last_rcons /= => [][]. elim: sn => [/= | sn /= IHsn]. by move/is_part_rconsK/IHs ->; rewrite size_rev incr_nth_size. move=> Hpart; rewrite {IHs}IHsn. - rewrite size_rev {Hpart}; elim: s => // s0 s IHs /=. by rewrite IHs. - exact: part_rcons_ind. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition