proposition: Lemma RinU (F : clause) : sf_closed F -> forall C, C \in powerset F -> R C \in powerset F.
proof: Proof. move => sfc_F C. rewrite !powersetE => /subP H. apply/subP => s. case: s => s [|]; last by rewrite (negbTE (Rpos _ _)). by rewrite RE => /H /sfc_F. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)