proposition: Lemma SsubU S : S `<=` S0 -> {subset S <= U}.
proof: Proof. move => sub_S. apply/subP. apply: sub_trans sub_S _. exact: subsep. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)