simpa using UTerm.fvar_primrec
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
this : Primcodable { t // t.bv ≤ n } := Primcodable.subtype ⋯
⊢ Primrec fun x => ↑(subtEquiv &x)
no goals