proposition: Lemma AR_rel_supp x y : AR_rel x (inl y) -> AR_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)