Theorem: LO.FirstOrder.Semiterm.lang_func (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
⊢ ⟨k, f⟩ ∈ (func f v).lang
Tactic:
simp[lang]
State after:
no goals