proposition: Lemma ref_R3 S C : S `<=` S0 -> coref F ref' S -> C \in S -> pAR 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: (fulfillsAREn C3 C2) => [[D D1 D2]|[C4 C5]]. - apply: ref_R2 (D1) _. apply: ref_R1 D2 => //. apply: ReqU D1 => //. by rewrite inE in C3; bcase. - rewrite (fset1U C1). apply: gen_AXn => /=. apply: gen_ARfoc. have/sfc_F/and3P [F1 F2 F3] : fAR s t^- \in F. { suff: C `<=` F. move/subP => /(_ _ C1). exact: sfc_F. rewrite -powersetE. by rewrite inE in C3; bcase. } apply: ref_R3_aux C5 => //. apply: RinU => //. 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)