proposition: Lemma evalP (w:M) s : reflect (@eval M s w) (evalb s w).
proof: Proof. elim: s w => //=. - by constructor. - move => * ; exact: idP. - move => s IHs t IHt w. apply: iffP (@implyP _ _) _ _ => ? /IHs ?; apply/IHt; firstorder. - move => s IHs w. apply: iffP (@forall_inP _ _ _) _ _ => H v /H /IHs; done. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)