simp[Encodable.encode_ofEquiv subtEquiv, Encodable.Subtype.encode_eq]
case pos
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 ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ encode (UTerm.func f fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = encode (func f fun i => l.get (Fin.cast ⋯ i))
case pos
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 ⋯
this : Primrec₂ fun f l => UTerm.funcL f (List.map (fun x => ↑(subtEquiv x)) l)
k : ℕ
f : L.Func k
l : List (Semiterm L μ n)
hl : l.length = k
⊢ (fun i => ↑(subtEquiv (l.get ⟨↑i, ⋯⟩))) = fun i => ↑(subtEquiv (l.get (Fin.cast ⋯ i)))