proposition: Lemma adm_P2 C p s : C \in S -> [p]s^- \in C -> ~~[some D in S, reach_demo S p C D && (s^- \in D)] -> href C.
proof: Proof. Proof using coref_S sfc_F sub_S. move => inS inC. rewrite -all_predC. move/allP => nR. set X := [fset D in S | [fset s^-] `<=` D]. have AAX: prv ([af C] ---> [p]\and_(D <- X) ~~:[af D]). { rewrite <- bigABBA. apply: bigAI => D. rewrite inE fsub1. case/andP => DinS inD. apply: (adm_P2_aux (u := s)) => //. - move/(subP sub_S) : inS inC. by rewrite inE powersetE => /andP [/subP H _] /H /flip_drop_sign. - move: (nR D DinS) => /=. by rewrite negb_and inD orbF. } have EOX: prv ([af C] ---> EX p (\or_(D <- X) [af D])). { rewrite <- rEXn; first by rewrite <- dmAX; exact: (bigAE _ inC). rewrite /X. rewrite <- (extension (C:= [fset s^-])). - apply: bigAI => t. rewrite inE. move/eqP => -> /=. exact: axI. - rewrite powersetE fsub1. apply: flipcl_refl. move/(subP sub_S) : inS inC. by rewrite inE powersetE => /andP [/subP H _] /H /flip_drop_sign /sfc_box. } rule axDup. rewrite -> EOX at 1. rewrite -> AAX. do 2 Intro. rule axB; last by do 2 Rev; exact: axDBD. rewrite -> rEXn; first exact: axnEXF. rewrite <- (axAcase (\or_(D<-X) [af D]) (\and_(D<-X) ~~: [af D]) Bot). apply: bigOE => D inX. rule axC. exact: bigAE. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)