proposition: Fact dio_rel_power_subst a b (R : nat -> (nat -> nat) -> Prop) : 𝔻F a -> 𝔻F b -> 𝔻R (fun ν => R (ν 0) (fun n => ν (S n))) -> 𝔻R (fun ν => R (power (a ν) (b ν)) ν).
proof: Proof. intros Ha Hb HR. by dio equiv (fun v => exists p, p = power (a v) (b v) /\ R p v). abstract(intros v; split; eauto; intros (? & ? & ?); subst; 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)