proposition: Theorem dio_elem_equation l : { E : dio_single nat nat | dio_single_size E <= 2+20*length l /\ forall ν, dio_single_pred E ν <-> exists φ, Forall (dc_eval φ ν) l }.
proof: Proof. destruct (dio_elem_single l) as (p & H1 & H2); exists p; split; auto. split; intros (phi & H); exists phi; revert H; apply H2. Defined.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)