proposition: Lemma AR_rel_term : terminates AR_rel.
proof: Proof. pose f (x : AR_T0) := if x is inl (SeqSub C rC) then (AR_level (ARlE rC)).+1 else 0. apply: (@terminates_measure _ f) => [[[C rC]|[C rC]]] [[D rD]|[D rD]] //=. case/and3P => _ _ ?. by rewrite ltnS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)