exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
  (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
case h
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
i : Fin k✝
⊢ ω₁ (v✝ i) = ω₂ (v✝ i)
no goals