proposition: Lemma MD_size n : fragment_bound FD n -> #|MD| <= n * (size (Fs D) * size D).
proof: Proof. move => bound_n. rewrite card_tagged. apply: leq_trans (@sumn_bound n _ _) _. - move => m. case/mapP => x H ->. exact: bound_n. - rewrite leq_mul2l size_map (eqP (tuple.enum_tupleP _)) card_prod. by rewrite !card_seq_sub ?funiq // leqnn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)