proposition: Lemma AR_ev_cond (x : seq_sub ARl) : exists2 y, connect AR_rel (inl x) y & AR_label y |> t^-.
proof: Proof. pose L x := AR_level (ARlE (ssvalP x)). move: {x} (L x).+1 {-2}x (ltnSn (L x)). elim => //. - move => n IHn x Hx. move: (level1 (monotone_fulfillAR_step S T s t) (ARlE (ssvalP x))). rewrite -/(AR_level _) /= inE. case/and3P => XinDD _. case/orP => [/hasP [E EinDD]|/hasP [E EinS0]]. + rewrite suppCU suppC1 => /andP[E_t E_R]. exists (inr (SeqSub E EinDD)) => //. apply: connect1. by case: x E_R {Hx XinDD}. + case/andP => suppE. case/level2 => rE bE. rewrite -!/(AR_level _) in bE. have El : E \in ARl. by rewrite inE EinS0. have/IHn [y y1 y2]: L (Sub E El) < n. rewrite /L [ARlE _](bool_irrelevance _ rE). apply: leq_trans bE _. by rewrite -ltnS. exists y => //. apply: connect_trans (connect1 _) y1. case: x bE suppE {XinDD Hx} => //= C rC E1 E2. by rewrite -suppC1 andbA -suppCU E2 [_ El](bool_irrelevance _ rE). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)