proposition: Fact dio_rel_fun_eq r t : 𝔻F r -> 𝔻F t -> 𝔻R (fun ν => r ν = t ν).
proof: Proof. intros H1 H2; red in H1, H2. apply dio_rel_equiv with (R := fun ν => exists x, x = r ν /\ x = t ν). + abstract (intros v; split; [ intros ->; exists (t v); auto | intros (? & -> & ?); auto ]). + apply dio_rel_exst, dio_rel_conj; auto. Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)