proposition: Corollary prv_dec s : decidable (prv s).
proof: Proof. case: (informative_completeness (~~: s)) => H; [left|right]. - by rule axDN. - move => prv_s. case: H => M _ [w]. apply. exact: (@soundness _ prv_s M). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)