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