proposition: Fact ra_dio_poly_eq_val : { e | ⟦ra_dio_poly_eq⟧ v e /\ (e = 0 <-> dp_eval φ ν p = dp_eval φ ν q) }.
proof: Proof. destruct ra_eq_rel with (v := dp_eval φ ν p ## dp_eval φ ν q ## vec_nil) as (e & H1 & H2); simpl in H2. exists e; split; auto. simpl. exists (dp_eval φ ν p ## dp_eval φ ν q ## vec_nil); split; auto. intros i; analyse pos i; simpl; apply ra_dio_poly_val. 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)