unfold fvar? at*
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : Function.funEqOn p.fvar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p