fact: Definition AR_rel (x y : AR_T0) := match x,y with | inl (SeqSub C rC),inl (SeqSub D rD) => [&& D |> s^-, suppC D (R C) & (AR_level (ARlE rD) < AR_level (ARlE rC))] | inl (SeqSub C rC),inr (SeqSub D rD) => suppC D (R C) | inr _,_ => false end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)