Remove n-ary Partrec' equivalence for smaller PR

Drop PartrecPrime.lean (1371 lines) which proved
URMComputable n ↔ Nat.Partrec'. This equivalence can still be
derived via Mathlib's Nat.Partrec'.part_iff combined with
the unary equivalence Partrec ↔ URMComputable1.

The unary equivalence in Partrec.lean + Simulate/ is the more
fundamental result that establishes URMs as a complete model
of computation.

Author: jessealama

Urm.lean

@@ -11,7 +11,6 @@ import Urm.Composition.Basic
 import Urm.PrimitiveRecursion.Basic
 import Urm.Minimization.Basic
 import Urm.Partrec
-import Urm.PartrecPrime
 import Urm.Simulate.Basic
 
 /-! # Public API
@@ -32,11 +31,9 @@ Core types and main theorems for URM computability.
 ## Main Theorems
 - `Urm.URMComputable1.toPartrec` - URM-computable implies Partrec (unary)
 - `Nat.Partrec.toURMComputable1` - Partrec implies URM-computable (unary)
-- `Urm.URMComputable_iff_Partrec'` - n-ary equivalence with Nat.Partrec'
 -/
 
 export Urm (Instr Program Config Step Steps)
 export Urm (URMComputable URMComputable1)
 export Urm (URMComputable1.toPartrec)
-export Urm (URMComputable_iff_Partrec')
 -- Note: Nat.Partrec.toURMComputable1 is in Nat namespace, auto-accessible