proposition: Corollary completeness s : valid s -> prv s.
proof: Proof. case: (informative_completeness (~~: s)) => [H|[M] _ [w] H] V. - by rule axDN. - exfalso. apply: H. exact: (V (cmodel_of_fmodel M)). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)