proposition: Lemma closed_sfc C : sf_closed (sfc C).
proof: Proof. exact: sfc_bigcup sfc_ssub. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)