fact: Definition step (D : {fset clause * annot}) : {fset clause * annot} := [fset A in U | [|| step_plain D A, step_annot D A| step_jmp D A ]].
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)