proposition: Theorem dio_elem_single l : { E : dio_single nat nat | dio_single_size E <= 2+20*length l /\ forall ν φ, dp_eval φ ν (fst E) = dp_eval φ ν (snd E) <-> Forall (dc_eval φ ν) l }.
proof: Proof. exists (dee2dp_1 l,dee2dp_2 l); split. + unfold dio_single_size, fst, snd. generalize (dee2dp_1_size l) (dee2dp_2_size l); intros; lia. + unfold dio_single_pred, fst, snd; split; apply dee2dp_spec. Defined.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)