Theorem: LO.FirstOrder.UFormula.elim_primrec_param (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
inst✝⁷ : (k : ℕ) → Primcodable (L.Func k)
inst✝⁶ : (k : ℕ) → Primcodable (L.Rel k)
inst✝⁵ : UniformlyPrimcodable L.Func
inst✝⁴ : UniformlyPrimcodable L.Rel
inst✝³ : Primcodable μ
σ : Type u_1
γ : Type u_2
inst✝² : Primcodable σ
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
γVerum γFalsum : σ → γ
γRel γNrel : σ → (k : ℕ) × L.Rel k × (Fin k → UTerm L μ) → γ
γAnd γOr : σ → γ × γ → γ
γAll γEx : σ → γ → γ
f : σ → UFormula L μ
hVerum : Primrec γVerum
hFalsum : Primrec γFalsum
hRel : Primrec₂ γRel
hNrel : Primrec₂ γNrel
hAnd : Primrec₂ γAnd
hOr : Primrec₂ γOr
hAll : Primrec₂ γAll
hEx : Primrec₂ γEx
hf : Primrec f
x✝ : σ
⊢ WType.elimL (fun p l => LO.FirstOrder.UFormula.F γVerum γFalsum γRel γNrel γAnd γOr γAll γEx x✝ (p, l))
      ((equivW L μ) (f x✝)) =
    elim (γVerum x✝) (γFalsum x✝) (fun {k} f v => γRel x✝ ⟨k, (f, v)⟩) (fun {k} f v => γNrel x✝ ⟨k, (f, v)⟩)
      (fun y₁ y₂ => γAnd x✝ (y₁, y₂)) (fun y₁ y₂ => γOr x✝ (y₁, y₂)) (γAll x✝) (γEx x✝) (f x✝)
Tactic:
simp[elim_eq]
State after:
no goals