proposition: Lemma ref_R4_aux s t (sF : s^+ \in F) (tF : t^+ \in F) S H C : coref F ref' S -> H `<=` U -> C \in U -> ~~ suppS S (t^+ |` C) -> (forall E, E \in base S0 (s^+ |` C) -> ~~ fulfillsAU S S0 s t E) -> gen (C,aAU (s,t,H)).
proof: Proof. move => coS subU. move: H subU C. apply: slack_ind => H IH subU C inU C1 C2. case: (boolP (C \in H)) => HC; first by rewrite (fset1U HC); exact: gen_AUrep. apply: gen_AUh. - apply: ref_R1 C1 => //. by rewrite powersetU inU powersetE fsub1 tF. - apply: ref_R0 => [|E in_base]; first by rewrite powersetU inU powersetE fsub1 sF. move/C2 : (in_base) => E1. case/sepP : in_base => E2 E3. case : (fulfillsAUEn E2 E1) => D [D1 D2 D3]. apply: ref_R2 (D1) _ => /=. apply: IH => //. + by rewrite fsubUset fsub1; bcase. + by rewrite fproper1. + apply: ReqU D1 => //. rewrite inE in E2. by 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)