proposition: Corollary valid_dec s : decidable (forall (M: cmodel) (w: M), eval s w).
proof: Proof. case (sat_dec (fImp s fF)) => /= H; [by firstorder|left => M w]. apply: modelP => A. apply: H. 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)