proposition: Fact dio_poly_eq_pos_equiv n (p q : dio_polynomial (pos n) P) ν : dio_single_pred (p,q) ν <-> exists w, dp_eval (vec_pos w) ν p = dp_eval (vec_pos w) ν q.
proof: Proof. split. + intros (w & Hw); exists (vec_set_pos w); eq goal Hw; f_equal; simpl; apply dp_eval_ext; auto; intros; rewrite vec_pos_set; auto. + intros (w & Hw); exists (vec_pos w); auto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)