proposition: Lemma sfc_bigcup (T : choiceType) (C : {fset T}) S : (forall s, sf_closed (S s)) -> sf_closed (\bigcup_(s in C) S s).
proof: Proof. move => H s. case/cupP => t /= /andP [T1 T2]. apply: sf_closed'_mon (H t s T2) _. exact: bigU1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)