induction t <;> simp[*, toSubLanguage', lMap_func]
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
no goals