fact: Record dmodel := DM { dstate :> choiceType ; dtrans : dstate -> dstate -> bool; dlabel : var -> pred dstate; dbound : dstate -> {fset dstate}; dtransP x y : dtrans x y -> y \in dbound x }.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)