proposition: Corollary fin_completeness s : (forall (M:fmodel) (w:M), eval s w) -> prv s.
proof: Proof. move => valid_s. case: (informative_completeness (~~: s)) => [|[M] _ [w] /=]; [by rewrite -> modular_hilbert.axDN|by firstorder]. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def dags demo hilbert relaxed_pruning)