proposition: Lemma or_S : prv (\or_(C <- S) [af C]).
proof: Proof. Proof using coref_S sfc_F. apply (rMP (s := [af fset0])). - rewrite -> extension; last by rewrite powersetE sub0x. apply: bigOE => C. rewrite inE. case/andP => inS _. exact: bigOI. - mp; last exact: axT. apply: bigAI => s. by rewrite inE. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)