proposition: Lemma maxS0 C s b : C \in S -> (s,b) \notin C -> s \in F -> (s,~~ b) \in C.
proof: Proof. Proof using sub_S. move/(subP sub_S). rewrite inE => /and3P[_ _ /allP] H inC /H. case: b inC => /negbTE-> //=. by rewrite orbF. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)