proposition: Lemma AU_this (s t : form) (L : DC) (inF : fAX (fAU s t)^+ \in Fs D) : let p := (SeqSub (fAX (fAU s t)^+) inF, L) in label (root (Frag p)) |> fAU s t^+ -> AU_M s t (Mstate (root (Frag p))).
proof: Proof. move => p. rewrite /=. case/orP => [?|/andP[E2 E3]]; first exact: AU0. move: (dmat_ev_cond p). rewrite /ev_cond /= E2 E3 /= => /(_ erefl) GL. elim: (sn_edge (root _)) => x _ IHsn. move: (GL x). case: (boolP (leaf x)) => nlf ?; first exact: AU0. apply: AUs => // [[p' y]]. rewrite /Mstate {1}/MRel (negbTE nlf) [_ && _]/= orbF => l_edge. move: (liftE l_edge) => ?; subst. rewrite lift_eq in l_edge. exact: IHsn. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)