proposition: Fact dio_rel_fun_sym x t : 𝔻F t -> 𝔻R (fun ν => t ν = ν x).
proof: Proof. intros H; dio_sym (dio_rel_fun x H). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)