proposition: Theorem dio_poly_eq_pos (e : dio_single nat P) : { m : nat & { p' : dio_polynomial (pos m) P & { q' | forall ν, dio_single_pred e ν <-> dio_single_pred (p',q') ν } } }.
proof: Proof. destruct e as (p,q). destruct (list_upper_bound (dp_var_list p++dp_var_list q)) as (m & Hm). destruct (@dio_poly_pos m p) as (p1 & H1). { intros; apply Hm, in_or_app; auto. } destruct (@dio_poly_pos m q) as (q1 & H2). { intros; apply Hm, in_or_app; auto. } exists m, p1, q1; intros psi; unfold dio_single_pred. split; intros (phi & Hphi). + exists (vec_pos (fun2vec 0 m phi)); simpl. rewrite <- H1, <- H2; auto. + exists (vec2fun (vec_set_pos phi) 0). rewrite H1, H2. rewrite fun2vec_vec2fun. eq goal Hphi; f_equal; apply dp_eval_ext; auto; intros j _; rewrite vec_pos_set; auto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)