proposition: Lemma Fs_size : size (Fs DD) <= size F.
proof: Proof. apply : subset_size. apply/subP => s. case/cupP => C /and3P[C1 _ C2]. move/(subP prune_sub) : C1. rewrite inE => /and3P [H _ _]. move: H. rewrite powersetE. by move/subP; apply. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)