simp[langFunc]
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (rel r v).langFunc
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → ∃ a, x ∈ (v a).lang