proposition: Lemma sfc_bigcup (T : choiceType) (C : {fset T}) F : (forall s, sf_closed (F s)) -> sf_closed (\bigcup_(s in C) F s).
proof: Proof. move => H. apply: big_rec => [s|i D _]; by [rewrite inE|exact: sfcU]. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)