proposition: Fact dio_rel_exst (K : nat -> (nat -> nat) -> Prop) : 𝔻R (fun ν => K (ν 0) ν⭳) -> 𝔻R (fun ν => exists x, K x ν).
proof: Proof. intros (f & Hf); exists (∃f). abstract (intros ν; rewrite df_pred_exst; split; intros (n & Hn); exists n; revert Hn; rewrite Hf; simpl; auto). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)