fact: Record sts := STS { state :> Type; trans : state -> state -> Prop; label : var -> state -> Prop; serial : forall w:state, exists v, trans w v }.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)