intro x (hx : x ∈ (v i).fv)
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ Function.funEqOn (fun x => x ∈ (v i).fv) f g
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁✝ : Type u_2
ξ₂✝ : Type u_3
ξ₃ : Type u_4
n n₁✝ n₂✝¹ n₂✝ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁✝ n₁✝ ξ₂✝ n₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x