proposition: Lemma serial_MRel (x : MType) : exists y, MRel x y.
proof: Proof. case: x => p x. case (boolP (leaf x)) => [lf|]. - have inF := label_DF lf. move: (root_internal (next p.1, SeqSub _ inF)). rewrite negbK => /existsP [y xy]. exists (Mstate y). by rewrite /MRel lf /Mstate xy /= !eqxx. - rewrite negbK => /existsP [y xy]. exists (Mstate y). by rewrite /MRel lift_eq xy. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)