proposition: Lemma fulfillsAUEn s t S C : C \in S0 -> ~~ fulfillsAU S S0 s t C -> exists D, [/\ D \in Req C , ~~ suppS S (t^+ |` D) & forall E, E \in base S0 (s^+ |` D) -> ~~ fulfillsAU S S0 s t E].
proof: Proof. move => inS. rewrite /fulfillsAU {1}fulfillsAUE inE inS /=. case/allPn => D D1. rewrite negb_or => /andP [S1 /hasPn S2]. exists D. split => // E. rewrite inE => /andP [E1 E2]. move: (S2 _ E1). by rewrite E2. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def demo gen_def relaxed_pruning)