proposition: Corollary sat_dec s : decidable (exists (M: cmodel) (w: M), eval s w).
proof: Proof. case: (informative_completeness s) => H; [right|left]. - case => M [w] Hw. exact: (@soundness _ H M). - case: H => M _ [w] ?. by exists M; exists w. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)