exact this.of_eq <| by intro x; generalize g x = t; induction t <;> simp[elim, bind, *]
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ Primrec fun x => bind (b x) (e x) (g x)
no goals