proposition: Lemma evalseq_decr_yam s : evalseq (decr_yam s) = behead (evalseq s).
proof: Proof. elim: s => //= s0 s IHs. case s0 => [| s0' /=]; rewrite IHs /=; case (evalseq s) => //. by case: s0'. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition