fact: Definition model_of_dmodel (M : dmodel) : cmodel := CModel (@dmodelP M).
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)