fact: Definition Mlabel (x: var) (C : Mtype) := fV x^+ \in val C.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)