proposition: Lemma DD_bounded_demo : bounded_demo S T (2 * size T).
proof: Proof. Proof using demoST. move => C u'. case: (evP C u') => [s t ->|s t ->|]; auto using frag_AR, frag_AU, simple_frag. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)