fact: Fixpoint evalb s : pred M := match s with | fV p => flabel p | fF => xpred0 | fImp s t => fun w => evalb s w ==> evalb t w | fAX s => fun w => [forall (v | ftrans w v) , evalb s v] end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)