fact: Record fmodel := FModel { fstate :> finType; ftrans : rel fstate; flabel : var -> pred fstate; fser w : exists v, ftrans w v }.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)