proposition: Lemma monotone_fulfillAR_step s t : monotone (fulfillAR_step s t).
proof: Proof. move => X Y X_sub_Y. apply: sep_sub; first exact: subxx. move => ? inS /=. case: [all _ in _ , _] => //=. case/orP =>[H|H];[by leftb|rightb]. 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)