proposition: Lemma fulfillsAU_DD s t L : L \in DD -> fAX (fAU s t)^+ \in L -> fulfillsAU DD S0 s t L.
proof: Proof. move => inDD inL. move: (inDD) => /pruneE. rewrite !negb_or. case/and3P => [_ H _]. move/hasPn : H => /(_ _ inL). by rewrite negbK. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)