case hex p ih => simp; exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
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✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom (∃' p) = (rewriteMap g).hom (∃' p)
no goals