proposition: Fact ra_dio_poly_prim p : prim_rec (ra_dio_poly p).
proof: Proof. induction p as [ | | | [] ]; simpl; repeat (split; auto); intros j; analyse pos j; simpl; 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)