proposition: Lemma AU_rel_succ (x : seq_sub AUl) D : D \in Req (ssval x) -> exists2 y, AU_rel (inl x) y & suppC (AU_label y) D.
proof: Proof. case: x => /= C /AUlE rC DinReq. move : (level1 (monotone_fulfillAU_step S T s t) rC). rewrite -!/(AU_level _). rewrite [iter _ _ _]/= {1}/fulfillAU_step inE. case/andP => XinDD. move/allP => /(_ _ DinReq). case/orP => [/hasP [E inDD]|/hasP [E inS0]]. - rewrite suppCU suppC1. case/andP => E_t E_D. have SE: E \in AUr. rewrite inE;bcase. exists (inr (SeqSub E SE)) => //. apply: suppC_sub E_D. exact: Req_RC. - rewrite suppCU suppC1 -andbA => /and3P [E_s E_D E_I]. case/level2 : (E_I) => rE L. rewrite -!/(AU_level _) in L. have SE: E \in AUl by rewrite inE inS0. exists (inl (SeqSub E SE)) => //. rewrite [AUlE SE](bool_irrelevance _ rE) L E_s /= andbT. apply: suppC_sub E_D. exact: Req_RC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)