proposition: Lemma monotone_fulfillAU_step s t : monotone (fulfillAU_step s t).
proof: Proof. move => X Y X_sub_Y. apply: sep_sub; first exact: subxx. move => ? inS /=. apply: sub_all => C /orP [H|H];[leftb|rightb]. - exact: sub_has H => L. - apply: sub_has H => L. case: (suppC _ _) => //=. exact: (subP X_sub_Y). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)