proposition: Lemma DD_small_model u L : u \in Fs DD -> L \in DD -> exists2 M : fmodel, #|M| <= size F * 2 ^ (2 * (size F) + 1) & exists (w : M), forall s : sform, L |> s -> eval (interp' s) w.
proof: Proof. move => inFs inDD. case: (small_models inFs demoDD_S0) => M M1 M2. exists M; last exact: M2. apply: leq_trans M1 _. rewrite addn1 [2 ^ _]expnS expnM -mulnn expnMn. rewrite !mulnA. rewrite leq_mul ?DD_size // ?[_ * 2]mulnC -?mulnA ?leq_mul2l. by rewrite leq_mul ?DD_size ?Fs_size. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)