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