Theorem: LO.FirstOrder.UTerm.elim_primrec_opt (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
γ : Type u_1
inst✝¹ : Inhabited γ
inst✝ : Primcodable γ
b : ℕ → γ
e : μ → γ
hb : Primrec b
he : Primrec e
u : {k : ℕ} → L.Func k → (Fin k → γ) → γ
uOpt : (k : ℕ) × L.Func k → List γ → Option γ
hu : Primrec₂ uOpt
H : ∀ {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt ⟨k, f⟩ (List.ofFn v) = some (u f v)
t : UTerm L μ
⊢ elim b e (fun {k} f v => (uOpt ⟨k, f⟩ (List.ofFn v)).iget) t = elim b e (fun {k} => u) t
Tactic:
simp[H]
State after:
no goals