proposition: Lemma ReqU L C : L \in U -> C \in Req L -> C \in U.
proof: Proof. Proof using sfc_F. move => inU. rewrite !inE. case/predU1P => [->|]; first by rewrite RinU. case/fimsetP => s. rewrite inE andbC. move: s => [[|p|? ?|s|? ?|? ?] [|]] //= inL ->. rewrite powersetU RinU // andbT powersetE fsub1. apply: Fsub inL inU. by rewrite /= !inE ssub_refl. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)