proposition: Fact dio_rel_fun x t : 𝔻F t -> 𝔻R (fun ν => ν x = t ν).
proof: Proof. apply dio_rel_ren with (ρ := fun n => match n with | 0 => x | S n => n end). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)