proposition: Lemma MRel_R (x y : MType) : MRel x y -> suppC (label (tagged y)) (R (label (tagged x))).
proof: Proof. case: x => p x. case: y => p' y. rewrite /MRel. case/orP => [H|]. - move: (liftE H) => ?; subst. rewrite lift_eq in H. exact: dag_R. - case/and4P => [_ /eqP Hp edg /eqP Hl] /=. move: (dag_R edg). by rewrite label_root -Hl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)