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] | fAU s t => AUb ftrans (evalb s) (evalb t) | fAR s t => ARb ftrans (evalb s) (evalb t) end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)