fact: Definition sf_closed (F :{fset sform}) := forall s, s \in F -> sf_closed' F s.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)