proposition: Corollary dio_rel_fractran_rt l x y : 𝔻F x -> 𝔻F y -> 𝔻R (fun ν => fractran_compute l (x ν) (y ν)).
proof: Proof. intros; apply dio_rel_rt; dio auto. Defined.
imports: List Arith Undecidability.Shared.Libs(utils_tac utils_list sums rel_iter gcd pos vec) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq) Undecidability.H10.Dio(dio_logic dio_bounded dio_rt_closure dio_single dio_expo)