fact: Record demo := Demo { cls :> {fset clause} ; demoD0 : D0 cls ; demoD1 : D1 cls ; demoD2 : D2 cls }.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)