proposition: Lemma DD_size : size S0 <= 2^(size F).
proof: Proof. rewrite -powerset_size. apply: subset_size. exact: subsep. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)