fact: Definition D1 cls := forall C, C \in cls -> forall s, fAX s^- \in C -> suppS cls (s^- |` R C).
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)