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

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
⊢ ∀ (a : L.Func k) (b : List (UTerm L μ)), funcL ⟨k, a⟩ b = funcL ⟨k, a⟩ b
Tactic:
intro f l
State after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
f : L.Func k
l : List (UTerm L μ)
⊢ funcL ⟨k, f⟩ l = funcL ⟨k, f⟩ l

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
f : L.Func k
l : List (UTerm L μ)
⊢ funcL ⟨k, f⟩ l = funcL ⟨k, f⟩ l
Tactic:
simp[WType.mkL, Edge]
State after:
no goals