have h : Primrec (fun f => ⟨f.1, f.2.1, (fun i => UTerm.subtEquiv (f.2.2 i))⟩
  : (k : ℕ) × L.Rel k × (Fin k → Semiterm L μ n) → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ)) :=
  encode_iff.mp (Primrec.encode.of_eq <| by
    rintro ⟨k, r, v⟩; simp[Encodable.encode_prod_val r, encode_finArrow']
    funext i; exact encode_ofEquiv subtEquiv _)
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
⊢ Primrec fun p => rel p.snd.1 p.snd.2
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
this : (n : ℕ) → Primcodable { t // t.bv ≤ n } := fun n => Primcodable.subtype ⋯
h : Primrec fun f => ⟨f.fst, (f.snd.1, fun i => ↑(subtEquiv (f.snd.2 i)))⟩
⊢ Primrec fun p => rel p.snd.1 p.snd.2