proposition: Lemma inU_sfc C : C \in powerset (sfc C).
proof: Proof. by rewrite powersetE sub_sfc. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)