proposition: Corollary small_models s : (exists (M:cmodel) (w:M), eval s w) -> (exists2 M : fmodel, #|M| <= f_size s * 2^(4 * f_size s + 2) & exists (w:M), eval s w).
proof: Proof. move => [M] [w] w_s. case: (informative_completeness s) => //. by move/soundness/(_ M w w_s). 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)