proposition: Lemma AU_lift (s t : form) (p : DF * DC) (x : Frag p) : (forall L', label (root (Frag (next p.1, L'))) |> fAU s t^+ -> AU_M s t (Mstate (root (Frag (next p.1, L'))))) -> label x |> fAU s t^+ -> AU_M s t (Mstate x).
proof: Proof. move => Hnext Lx. move: (sn_edge x) Lx. elim => {x} - x _ IH Lx. case: (boolP (leaf x)) => [lf|Hx]. + apply: leaf_root. apply: Hnext => //. by rewrite label_root. + rewrite /= in Lx. case/orP : Lx => [Lx|/andP [L1 L2]]. exact: AU0. apply: AUs => // [[p' y]]. rewrite /Mstate {1}/MRel (negbTE Hx) [_ && _]/= orbF => l_edge. move: (liftE l_edge) => ?; subst. rewrite lift_eq in l_edge. apply: IH (l_edge) _. exact: supp_edge l_edge. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)