proposition: Lemma leaf_root_aux (p : DF * DC) (x : Frag p) (lf : leaf x) : forall y, MRel (Mstate (root (Frag (next p.1, SeqSub (label x) (label_DF lf))))) y <-> MRel (Mstate x) y.
proof: Proof. move => [p' y]. rewrite /MRel /Mstate (negbTE (root_internal _)) [_ && _]/= orbF. split => [le|/orP [le|H]]. - move: (liftE le) => ?;subst. rightb. rewrite lf /= !eqxx. by rewrite lift_eq in le. - move: (liftE le) => ?;subst. rewrite lift_eq in le. suff: false by []. rewrite -(negbTE lf). apply/existsP. by eexists. - case/and4P : H => _. destruct p as [u L]. destruct p' as [u' L']. move/eqP => /= ? e; subst. move/eqP => Lx. move: (label_DF lf). rewrite Lx => inDF. rewrite [SeqSub _ _](_ : _ = L') ?lift_eq //. apply/eqP. destruct L'. exact: eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)