proposition: Theorem ra_dio_poly_find_spec_strong2 v w : dp_eval (vec_pos v) (vec_pos w) p = dp_eval (vec_pos v) (vec_pos w) q -> exists e, ⟦ra_dio_poly_find⟧ w e.
proof: Proof. intros. eapply ra_dio_poly_find_spec. eauto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec) Undecidability.MuRec.Util(recalg ra_utils recomp ra_recomp) Undecidability.H10.Dio(dio_single)