proposition: Lemma ref_R4 S C : S `<=` S0 -> coref F ref' S -> C \in S -> pAU F C S -> ref' C.
proof: Proof. move => S1 S2 inS. case/hasP. do 3 case => //. move => s t [|//] C1 C2. move/(subP S1) : inS => C3. case (fulfillsAUEn C3 C2) => E [E1 E2 E3]. apply: ref_R2 (E1) _ => /=. have inE': fAU s t^+ \in E. apply: (subP (Req_RC E1)). by rewrite RE. have inF: fAU s t^+ \in F. suff: E `<=` F by move/subP; apply. rewrite -powersetE. apply: ReqU E1 => //. by rewrite inE in C3; bcase. rewrite (fset1U inE'). apply: gen_AUfoc. apply: ref_R4_aux E2 _ => //. - move/sfc_F : inF => /=. by bcase. - move/sfc_F : inF => /=. by bcase. - apply: ReqU E1 => //. by rewrite inE in C3; bcase. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def demo gen_def relaxed_pruning)