proposition: Theorem dio_rel_is_seq c q n : 𝔻F c -> 𝔻F q -> 𝔻F n -> 𝔻R (fun ν => is_seq R (c ν) (q ν) (n ν)).
proof: Proof. Proof using HR. intros H1 H2 H3. unfold is_seq. apply dio_rel_fall_lt; dio auto. Defined.
imports: Arith List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list rel_iter sums) Undecidability.H10.Dio(dio_logic dio_expo dio_bounded)