exact ih i (he.of_subset $ by simp[fvar?]; intro x hx; exact ⟨i, hx⟩)
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ω₁ (v i) = ω₂ (v i)
no goals