proposition: Lemma fulfillAGEn s S C : ~ fulfillAG S s C -> forall D, D \in S -> rtrans C D -> ~~ D |> s^- /\ ~ fulfillAG S s D.
proof: Proof. move => H D CD. split => [|Ds]; last by apply: H; apply: fulfillAGn Ds. apply/negP => Ds. apply H. exact: fulfillAG1 Ds. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)