fact: Definition ts_of_dmodel (M : dmodel) : ts := {| state := dstate M; trans := @dtrans M ; label p x := @dlabel M p x |}.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)