induction p using rec' <;> simp[*, toSubLanguage', lMap_rel, lMap_nrel]
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
pf : (k : ℕ) → L.Func k → Prop
pr : (k : ℕ) → L.Rel k → Prop
n : ℕ
p : Semiformula L μ n
hf : ∀ (k : ℕ) (f : L.Func k), ⟨k, f⟩ ∈ p.langFunc → pf k f
hr : ∀ (k : ℕ) (r : L.Rel k), ⟨k, r⟩ ∈ p.langRel → pr k r
⊢ (lMap L.ofSubLanguage) (toSubLanguage' pf pr p hf hr) = p
no goals