proposition: Lemma EU_lift (s t : form) (p : DF * DC) (x : Frag p) : (forall L', label (root (Frag (next p.1, L'))) |> fAR s t^- -> EU_M s t (Mstate (root (Frag (next p.1, L'))))) -> label x |> fAR s t^- -> EU_M s t (Mstate x).
proof: Proof. move => Hnext Lx. move: (sn_edge x) Lx. elim => {x} - x _ IH Lx. rewrite /= in Lx. case/orP : Lx => [Lx|/andP [L1 L2]]. exact: EU0. case: (boolP (leaf x)) => [lf|Hx]. + apply: leaf_root'. apply: Hnext => //. by rewrite label_root /=; bcase. + case: (dag_D Hx L2) => y xy Hy. apply: (EUs (v := Mstate y)) => //; [by rewrite /MRel lift_eq xy|exact: IH]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)