proposition: Lemma dio_rel_compose : 𝔻R (fun ν => R (f ν) ν).
proof: Proof. Proof using HR Hf. by dio equiv (fun v => exists y, y = f v /\ R y v). abstract(intros v; split; [ exists (f v); auto | intros (? & -> & ?); auto ]). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)