proposition: Theorem ra_dio_poly_find_spec_strong1 e w : ⟦ra_dio_poly_find⟧ w e -> dp_eval (vec_pos (project n e)) (vec_pos w) p = dp_eval (vec_pos (project n e)) (vec_pos w) q.
proof: Proof. intros Hx % ra_dio_poly_find_rel_strong1. rename e into x. destruct (ra_dio_poly_test_val x w) as (e & H1 & H2). assert (e = 0). eapply (ra_rel_fun _ _ _ _ H1 Hx); rewrite H2. eapply H2 in H. eq goal H; f_equal; apply dp_eval_ext; intro; try rewrite vec_pos_app_left; auto; rewrite vec_pos_app_right; auto. 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)