proposition: Lemma EU_this (s t : form) (L : DC) (inF : fAX (fAR s t)^- \in Fs D) : let p := (SeqSub (fAX (fAR s t)^-) inF, L) in label (root (Frag p)) |> fAR s t^- -> EU_M s t (Mstate (root (Frag p))).
proof: Proof. move => p. rewrite /=. case/orP => [?|/andP[E2 E3]]; first exact: EU0. move: (dmat_ev_cond p). rewrite /ev_cond /= E2 E3 /= => /(_ erefl) [E4 [z]]. case/connectP : (rootP z) => xs. elim: xs (root _) => [x|y ys IHys x /=]. - move => _ -> /= ?. exact: EU0. - case/andP => xy pth ? ?. have M: MRel (Mstate x) (Mstate y) by rewrite /MRel lift_eq; bcase. apply: EUs (M) _ => //=; last exact: IHys. apply: E4. rewrite negbK. by apply/existsP; eexists. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)