proposition: Corollary dio_rel_single R : 𝔻R R -> { E : dio_single nat nat | forall ν, R ν <-> dio_single_pred E ν}.
proof: Proof. intros (A & HA). destruct dio_formula_elem with (f := A) as (l & _ & _ & Hl). destruct dio_elem_equation with (l := l) as (E & _ & HE). exists E; intro; rewrite HE, <- Hl, HA; tauto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)