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

State before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n : ℕ
pf : (k : ℕ) → L.Func k → Prop
pr : (k : ℕ) → L.Rel k → Prop
t : Semiterm L μ n
h : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ t.lang → pf k f
⊢ lMap L.ofSubLanguage (toSubLanguage' pf pr t h) = t
Tactic:
induction t <;> simp[*, toSubLanguage', lMap_func]
State after:
no goals