proposition: Lemma tref_R3 S C s : S `<=` S0 -> coref F tref S -> C \in S -> fAX (fAG s)^- \in C -> ~ fulfillAG S0 S s C -> tref C.
proof: Proof. Proof using sfc_F. move => subS0 corefS inS inC H. have {H} AGn : C \notin fulfillAGb S0 S s by apply/fulfillAGP; tauto. have inF: s^- \in F. move/(subP subS0)/(subP subsep) : inS => inU. rewrite powersetE in inU. move/(subP inU)/sfc_F/sfc_F : inC => //=. by case/andP. rewrite (fset1U inC). apply: gen_foc => {inC}. apply (subP subS0) in inS. move: fset0 (sub0x U) C inS AGn. apply: slack_ind => H IH subU C inS. rewrite -[{fset _}]/{fset clause} in IH. have /andP [inU RU] : (C \in U) && (R C \in U). move/(subP subsep) : inS => inU. by rewrite RinU. rewrite fulfillAGE inE inS //= negb_and negb_or. case/orP. - case/allPn => ? /fimsetP [?]. rewrite inE andbC. case:(isDiaP _) => //= t -> inC -> /= sRs. rewrite (fset1U inC). apply gen_AXn. apply: tref_R1 sRs => //. suff: fAX t^- \in F. move/sfc_F => ?. by rewrite powersetU RU powersetE fsub1. by apply/powersetP : inC. - case/andP => H1 /hasPn H2. constructor. case: (boolP (R C \in H)) => HR; first by rewrite (fset1U HR); exact: gen_rep. apply: gen_AGh. + apply: tref_R1 H1 => //. by rewrite powersetU powersetE fsub1 inF. + apply: tref_R0 (RU) _ => D /sepP [D1 D2]. apply: IH (D1) _; rewrite ?fsubUset ?fsub1 ?fproper1; try bcase. move: (H2 _ D1). by rewrite /rtrans D2. Qed.
imports: Relations Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def demo hilbert_ref gen_def)