proposition: Lemma AR_rel_succ (x : seq_sub ARl) D : D \in Req (ssval x) -> exists2 y, AR_rel (inl x) y & suppC (AR_label y) D.
proof: Proof. move: (ssvalP x). rewrite inE => /andP[_ S2] inReq. rewrite /fulfillsAR fulfillsARE inE in S2. case/and3P : S2 => _ /allP S2 _. move: S2 => /(_ _ inReq). case/hasP => [E E1 E2]. exists (inr (SeqSub E E1)) => //=. case: x inReq => //= C _ /Req_RC H. exact: suppC_sub E2. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)