proposition: Lemma AU_rel_supp x y : AU_rel x (inl y) -> AU_label (inl y) |> s^+.
proof: Proof. case: x => // x. case: x => ? ?; case: y => ? ? /=; bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)