proposition: Lemma RinU F a : sf_closed F -> forall C, C \in powerset (flipcl F) -> R a C \in powerset (flipcl F).
proof: Proof. move => sfc_F C. rewrite !powersetE => /subP H. apply/subP => s. case: s => s [|]; last by rewrite (negbTE (Rpos _ _ _)). rewrite RE /flipcl => /H /flip_drop_sign /= inF. apply/cupP. exists s. rewrite !inE /= andbT. exact: (sfc_F [pV a]s). Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)