proposition: Fact dio_rel_ren R ρ : 𝔻R R -> 𝔻R (fun ν => R (fun n => ν (ρ n))).
proof: Proof. intros (f & Hf); exists (f⦃ρ⦄). abstract (intros; rewrite df_pred_ren, Hf; tauto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)