proposition: Lemma extension C : C \in PU -> prv ([af C] ---> \or_(D <- [fset D in S | C `<=` D]) [af D]).
proof: Proof. Proof using coref_S sfc_F. move => Csub. rewrite -> extension0 => //. apply: bigOE => D. rewrite !inE. case/andP => /and3P [Dsub M H] CsubD. case inS: (D \in S). - apply: bigOI. by rewrite !inE inS CsubD. - rewrite -> coref_S; first exact: axBE. by rewrite !inE Dsub M H inS. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)