exact (w_elimL_param hF (Primrec.of_equiv.comp ht)).of_eq (fun x => by simp[elim_eq])
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 γ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
hu : Primrec₂ u
ht : Primrec t
hF : Primrec₂ (LO.FirstOrder.UTerm.F b e u)
⊢ Primrec fun x => elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (t x)
no goals