proposition: Lemma model_existence u L : u \in Fs D -> L \in D -> exists (M : fmodel) (w : M), forall s, L |> s -> eval (interp' s) w.
proof: Proof. Proof using Dl FD. move => inF inDF. exists MD. 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)