proposition: Lemma neg_or A : A `<=` S -> prv ((~~: \or_(C <- A) [af C]) ---> \or_(C <- S `\` A) [af C]).
proof: Proof. Proof using coref_S sfc_F. move => sub. mp; last exact: or_S. apply: bigOE => C inS. case inA: (C \in A). - rewrite <- (bigOI _ inA). exact: axContra. - rule axC. drop. apply: bigOI. by rewrite inE inS inA. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)