proposition: Lemma ref_R3_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) -> ~~ fulfillsAR S S0 s t E) -> gen (C,aAR (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_ARrep. apply: gen_ARh. - apply: ref_R1 C1 => //. by rewrite powersetU inU powersetE fsub1 tF. - apply: ref_R0 => [|E in_base]. by rewrite powersetU inU powersetE fsub1 sF. move/C2 : (in_base) => E1. case/sepP : in_base => E2 E3. case: (fulfillsAREn E2 E1) => [[D D1 D2]|[D1 D2]]. + apply: ref_R2 (D1) _ => /=. apply: ref_R1 D2 => //. apply: ReqU D1 => //. by rewrite inE in E2; bcase. + apply: gen_aAXR. apply: IH => //. + by rewrite fsubUset fsub1; bcase. + by rewrite fproper1. + apply: RinU _ => //. 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)