Theorem: LO.FirstOrder.UTerm.elim_primrec_param_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
γ : Type u_2
inst✝² : Primcodable σ
inst✝¹ : Inhabited γ
inst✝ : Primcodable γ
b : σ → ℕ → γ
e : σ → μ → γ
t : σ → UTerm L μ
hb : Primrec₂ b
he : Primrec₂ e
u : σ → {k : ℕ} → L.Func k → (Fin k → γ) → γ
uOpt : σ → ((k : ℕ) × L.Func k) × List γ → Option γ
hu : Primrec₂ uOpt
ht : Primrec t
H : ∀ (x : σ) {k : ℕ} (f : L.Func k) (v : Fin k → γ), uOpt x (⟨k, f⟩, List.ofFn v) = some (u x f v)
x✝ : σ
⊢ elim (b x✝) (e x✝) (fun {k} f v => (uOpt x✝ (⟨k, f⟩, List.ofFn v)).iget) (t x✝) =
    elim (b x✝) (e x✝) (fun {k} => u x✝) (t x✝)
Tactic:
simp[H]
State after:
no goals