proposition: Lemma MRel_D (x : MType) s : fAX s^- \in label (tagged x) -> exists2 y, MRel x y & label (tagged y) |> s^-.
proof: Proof. case: x => p x. case (boolP (leaf x)) => lf Ls. - have inF := label_DF lf. move: (root_internal (next p.1, SeqSub _ inF)) => H. set p' := (_,_) in H. have Ls' : fAX s^- \in label (root (Frag p')) by rewrite label_root /=. case: (dag_D H Ls') => y Hy Lys. by exists (Mstate y); rewrite // /Mstate /MRel Hy /p' lf /= !eqxx. - case: (dag_D lf Ls) => y Hy Lys. by exists (Mstate y); rewrite // /Mstate /MRel lift_eq Hy. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)