proposition: Lemma small_model_existence u L n : fragment_bound FD n -> u \in Fs D -> L \in D -> exists2 M : fmodel, #|M| <= n * (size (Fs D) * size D) & exists (w : M), forall s, L |> s -> eval (interp' s) w.
proof: Proof. move => bound_n inF inDF. exists MD; first exact: MD_size. pose p := (SeqSub _ inF, SeqSub _ inDF). exists (Mstate (root (Frag p))). move => s supp_s. apply: supp_eval. by rewrite /= label_root. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)