proposition: Fact ra_dio_poly_test_rel v e : ⟦ra_dio_poly_test p q⟧ v e -> e = 0 <-> dp_eval (φ (vec_head v) (vec_tail v)) (ν (vec_head v) (vec_tail v)) p = dp_eval (φ (vec_head v) (vec_tail v)) (ν (vec_head v) (vec_tail v)) q.
proof: Proof. vec split v with x; intros H; simpl vec_head; simpl vec_tail. destruct (ra_dio_poly_test_val x v) as (e' & H1 & H2). rewrite <- H2; clear H2. generalize (ra_rel_fun _ _ _ _ H H1); intros []; tauto. 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)