proposition: Lemma R3 C s : C \in S -> fAX (fAG s)^- \in C -> ~ fulfillAG S s C -> ref C.
proof: Proof. Proof using coref_S sfc_F sub_S. move => CinS inC nsupp_s. rewrite (fset1U inC). apply: refI1n. pose I := [fset D in S | D \notin fulfillAGb s S]. pose u := \or_(D <- I) [af D]. have IP D : D \in I -> ~~ suppS S (s^- |` R D) /\ {subset base S (R D) <= I}. case/sepP => inS. rewrite fulfillAGE inE inS /= => /hasPn H. split. + apply/hasPn => D' inS'. move: (H _ inS'). rewrite suppCU suppC1 /rtrans. by apply contraNN => /andP [-> ->]. + move => D' /sepP [D1 D2]. rewrite inE D1 /=. move: (H _ D1). rewrite /rtrans D2 /= negb_or. by case/andP. Cut u; first by apply: (bigOI xaf); rewrite inE CinS /=; apply/negP => /fulfillAGP; tauto. apply: rAGp_ind. apply: bigOE => D inI. rewrite -> box_request. apply: rNorm. have HR : R D \in U. rewrite RinU //. rewrite inE in inI. case/andP : inI => /(subP sub_S) H _. rewrite inE /U in H. by case/and3P: H. ApplyH axAI. - rewrite -> baseP => //. apply: or_sub. by apply IP. - apply: refE1n. apply: R1; last by apply IP. rewrite powersetU HR powersetE fsub1 andbT. move/(subP sub_S) : CinS. rewrite inE => /and3P [X _ _]. rewrite powersetE in X. move/(subP X) : inC. move => /sfc_F /= /sfc_F /=. by case/andP => _ ->. Qed.
imports: Relations Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def demo)