fact: Record ts := TS { state :> Type; trans : state -> state -> Prop; label : var -> state -> Prop }.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)