proposition: Lemma DD_demo_aux : { FRAG : fragment_demo S T | fragment_bound FRAG (2 * size T) }.
proof: Proof. Proof using demoST. pose FRAG L u (inFs : u \in Fs S) (inDD : L \in S) := let G := DD_bounded_demo inFs inDD in exist _ (s2val G) (s2valP G). exists (FragmentDemo FRAG (demoSsubT demoST) (demoT demoST)). move => /= L u inFs inD. rewrite /FRAG /=. exact: (s2valP' (DD_bounded_demo inFs inD)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)