proposition: Lemma hyper_yam_of_eval ev : is_part ev -> is_yam_of_eval ev (hyper_yam ev).
proof: Proof. by move=> H; rewrite /is_yam_of_eval (hyper_yamP H) (evalseq_hyper_yam H) /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition